Mercurial > hg > Members > kono > Proof > automaton1

changeset 4:2d8d29454b0f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Nov 2020 10:41:38 +0900
parents bf6d7843ba11
children 06cc23ff53d7
files nfa.agda
diffstat 1 files changed, 16 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/nfa.agda	Sat Nov 14 09:58:56 2020 +0900
+++ b/nfa.agda	Sat Nov 14 10:41:38 2020 +0900
@@ -28,13 +28,14 @@
 
 ntrace : {n  : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set)  → Set) → (nfa : NAutomaton Q Σ) → (qs : Q → Set ) → (input : List Σ )
      → naccept Nexists nfa qs input
-     → ((qs : Q → Set) (q : Q) → Dec (qs q ∧ NF nfa q))
-     → ((qs : Q → Set) (x : Σ) (t : List Σ) (q : Q) → Dec (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q') t))
+     → ((qs : Q → Set) (a : Nexists (λ q → qs q ∧ NF nfa q)) (q : Q)  → Dec (qs q ∧ NF nfa q))
+     → ((qs : Q → Set) (x : Σ) (t : List Σ) (a : naccept Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q')) t)
+          (q : Q) → Dec (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q') t))
      → List Q
      → List (List Q)
-ntrace {n} {Q} {Σ} Nexists nfa qs [] a decNF decNδ L = qlist (λ q → qs q ∧ NF nfa q) (decNF qs) L ∷ []
+ntrace {n} {Q} {Σ} Nexists nfa qs [] a decNF decNδ L = qlist (λ q → qs q ∧ NF nfa q) (decNF qs a) L ∷ []
 ntrace {n} {Q} {Σ} Nexists nfa qs (x ∷ t) a decNF decNδ L = 
-      qlist (λ q → (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q' ) t )) (decNδ qs x t) L
+      qlist (λ q → (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q' ) t )) (decNδ qs x t a ) L
       ∷ ( ntrace Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a decNF decNδ L )
 
 data transition136 : Q3  → Σ2  → Q3 → Set  where
@@ -65,20 +66,20 @@
 Q3List : List Q3
 Q3List = q₁ ∷ q₂ ∷ q₃ ∷ []
 
-decFN136 : (qs qs' : Q3 → Set)  → (x : List Σ2) → naccept exists-in-Q3 nfa136 qs x → (q : Q3) → Dec (qs' q ∧ NF nfa136 q)
-decFN136 qs qs' (_ ∷ _)  _ _ = {!!}
-decFN136 qs qs' [] (qe1 x) q₁ = yes [ {!!} , refl ]
-decFN136 qs qs' []  _ q₂ = no (λ ())
-decFN136 qs qs' []  _ q₃ = no (λ ())
+decFN136 : (qs' : Q3 → Set)  → (q : Q3) →  exists-in-Q3 (λ q' → qs' q' ∧ (q' ≡ q₁)) → Dec (qs' q ∧ NF nfa136 q)
+decFN136 qs' q₁ (qe1 x) = yes x
+decFN136 qs' q₂ _ = no (λ ())
+decFN136 qs' q₃ _ = no (λ ())
 
-decF̨δ136 :  (qs qs' : Q3 → Set) (s : Σ2) (t x : List Σ2) → naccept exists-in-Q3 nfa136 qs x → (q : Q3) →
-    Dec (naccept exists-in-Q3 nfa136 (λ q' → qs' q ∧ Nδ nfa136 q s q') t)
-decF̨δ136 qs qs' s t x a q₁ = {!!}
-decF̨δ136 qs qs' s t x a q₂ = {!!}
-decF̨δ136 qs qs' s t x a q₃ = {!!}
+decF̨δ136 :  (qs' : Q3 → Set) (s : Σ2) (t : List Σ2) 
+    → (a : naccept exists-in-Q3 nfa136 (λ q' → exists-in-Q3 (λ q₄ → qs' q₄ ∧ transition136 q₄ s q')) t)
+    → (q : Q3) → Dec (naccept exists-in-Q3 nfa136 (λ q' → qs' q ∧ Nδ nfa136 q s q') t)
+decF̨δ136 qs' s t a q₁ = ?
+decF̨δ136 qs' s t a q₂ = {!!}
+decF̨δ136 qs' s t a q₃ = {!!}
 
 nfa136trace : (qs : Q3 → Set) → (input : List Σ2 ) → naccept exists-in-Q3 nfa136 qs input → List (List Q3)
-nfa136trace qs x a = ntrace exists-in-Q3 nfa136 qs x a (λ qs' q → decFN136 qs qs' x a q ) (λ qs' s t q →  decF̨δ136 qs qs' s t x a q ) Q3List
+nfa136trace qs x a = ntrace exists-in-Q3 nfa136 qs x a (λ qs' a' q → decFN136 qs' q a' ) (λ qs' s t a' q →  decF̨δ136 qs' s t a' q ) Q3List
 
 subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → (Nexists : (Q → Set)  → Set) → 
     (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ