# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1541410643 -32400
# Node ID cd311109d63b833bbd7404cfa1a17454c99505af
# Parent  9b00dc130ede6b35566bff56c9febf001c3bb642
suset construction for subset function nfa

diff -r 9b00dc130ede -r cd311109d63b agda/sbconst2.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/sbconst2.agda	Mon Nov 05 18:37:23 2018 +0900
@@ -0,0 +1,32 @@
+module sbconst2 where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+open import Data.List
+open import Data.Bool using ( Bool ; true ; false ; _∧_ )
+
+open import automaton
+open import nfa
+open NAutomaton
+open Automaton
+open FiniteSet
+
+δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
+δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → nδ r i q )
+
+subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  
+    (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )  
+subset-construction {Q} { Σ} {n} N NFA = record {
+        δ = λ q x → δconv N ( Nδ NFA ) q x
+     ;  astart = astart1
+     ;  aend = aend1
+   } where
+     astart1 : Q → Bool
+     astart1 = Nstart NFA 
+     aend1 : (Q → Bool) → Bool
+     aend1 f = exists N ( λ q → f q ∧ Nend NFA q )
+
+test4 = subset-construction finState1 am2
+
+test5 = accept test4  ( i0  ∷ i1  ∷ i0  ∷ [] )
+test6 = accept test4  ( i1  ∷ i1  ∷ i1  ∷ [] )