Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/nfa.agda @ 406:a60132983557

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 Wed, 08 Nov 2023 21:35:54 +0900
parents af8f630b7e60
children 207e6c4e155c
comparison
equal deleted inserted replaced
405:af8f630b7e60 406:a60132983557
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2 -- {-# OPTIONS --allow-unsolved-metas #-}
2 module nfa where 3 module nfa where
3 4
4 -- open import Level renaming ( suc to succ ; zero to Zero ) 5 -- open import Level renaming ( suc to succ ; zero to Zero )
5 open import Data.Nat 6 open import Data.Nat
6 open import Data.List 7 open import Data.List
52 → NAutomaton Q Σ 53 → NAutomaton Q Σ
53 → (exists : ( Q → Bool ) → Bool) 54 → (exists : ( Q → Bool ) → Bool)
54 → ( Qs : Q → Bool ) → (s : Σ ) → ( Q → Bool ) 55 → ( Qs : Q → Bool ) → (s : Σ ) → ( Q → Bool )
55 Nmoves {Q} { Σ} M exists Qs s = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q ) )) 56 Nmoves {Q} { Σ} M exists Qs s = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q ) ))
56 57
58 --
59 -- Q is finiteSet
60 -- so we have
61 -- exists : ( P : Q → Bool ) → Bool
62 -- which checks if there is a q in Q such that P q is true
63
57 Naccept : { Q : Set } { Σ : Set } 64 Naccept : { Q : Set } { Σ : Set }
58 → NAutomaton Q Σ 65 → NAutomaton Q Σ
59 → (exists : ( Q → Bool ) → Bool) 66 → (exists : ( Q → Bool ) → Bool)
60 → (Nstart : Q → Bool) → List Σ → Bool 67 → (Nstart : Q → Bool) → List Σ → Bool
61 Naccept M exists sb [] = exists ( λ q → sb q /\ Nend M q ) 68 Naccept M exists sb [] = exists ( λ q → sb q /\ Nend M q )
62 Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t 69 Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t
63 70
64 {-# TERMINATING #-} 71 -- {-# TERMINATING #-}
65 NtraceDepth : { Q : Set } { Σ : Set } 72 -- NtraceDepth : { Q : Set } { Σ : Set }
66 → NAutomaton Q Σ 73 -- → NAutomaton Q Σ
67 → (Nstart : Q → Bool) → (all-states : List Q ) → List Σ → List (List ( Σ ∧ Q )) 74 -- → (Nstart : Q → Bool) → (all-states : List Q ) → List Σ → List (List ( Σ ∧ Q ))
68 NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where 75 -- NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where
69 ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (List ( Σ ∧ Q ) ) → List (List ( Σ ∧ Q ) ) 76 -- ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (List ( Σ ∧ Q ) ) → List (List ( Σ ∧ Q ) )
70 ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( List ( Σ ∧ Q )) → List ( List ( Σ ∧ Q )) 77 -- ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( List ( Σ ∧ Q )) → List ( List ( Σ ∧ Q ))
71 ndepth1 q i [] is t t1 = t1 78 -- ndepth1 q i [] is t t1 = t1
72 ndepth1 q i (x ∷ qns) is t t1 = ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 ) 79 -- ndepth1 q i (x ∷ qns) is t t1 = ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
73 ndepth [] sb is t t1 = t1 80 -- ndepth [] sb is t t1 = t1
74 ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q 81 -- ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
75 ... | true = ndepth qs sb [] t ( t ∷ t1 ) 82 -- ... | true = ndepth qs sb [] t ( t ∷ t1 )
76 ... | false = ndepth qs sb [] t t1 83 -- ... | false = ndepth qs sb [] t t1
77 ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q 84 -- ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q
78 ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 ) 85 -- ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
79 ... | false = ndepth qs sb (i ∷ is) t t1 86 -- ... | false = ndepth qs sb (i ∷ is) t t1
80
81 NtraceDepth1 : { Q : Set } { Σ : Set }
82 → NAutomaton Q Σ
83 → (Nstart : Q → Bool) → (all-states : List Q ) → List Σ → Bool ∧ List (List ( Σ ∧ Q ))
84 NtraceDepth1 {Q} {Σ} M sb all is = ndepth all sb is [] [] where
85 exists : (Q → Bool) → Bool
86 exists p = exists1 all where
87 exists1 : List Q → Bool
88 exists1 [] = false
89 exists1 (q ∷ qs) with p q
90 ... | true = true
91 ... | false = exists1 qs
92 ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (Bool ∧ List ( Σ ∧ Q ) ) → Bool ∧ List (List ( Σ ∧ Q ) )
93 ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( Bool ∧ List ( Σ ∧ Q )) → List ( Bool ∧ List ( Σ ∧ Q ))
94 ndepth1 q i [] is t t1 = t1
95 ndepth1 q i (x ∷ qns) is t t1 = ? -- ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
96 ndepth [] sb is t t1 = ? -- ⟪ exists (λ q → Nend M q /\ sb q) ? ⟫
97 ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
98 ... | true = ndepth qs sb [] t ( ? ∷ t1 )
99 ... | false = ndepth qs sb [] t t1
100 ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q
101 ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
102 ... | false = ndepth qs sb (i ∷ is) t t1
103 87
104 -- trace in state set 88 -- trace in state set
105 -- 89 --
106 Ntrace : { Q : Set } { Σ : Set } 90 Ntrace : { Q : Set } { Σ : Set }
107 → NAutomaton Q Σ 91 → NAutomaton Q Σ
154 example2-2 = Naccept am2 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) 138 example2-2 = Naccept am2 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] )
155 139
156 t-1 : List ( List States1 ) 140 t-1 : List ( List States1 )
157 t-1 = Ntrace am2 LStates1 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ (sr ∷ ss ∷ st ∷ []) ∷ (st ∷ []) ∷ [] 141 t-1 = Ntrace am2 LStates1 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ (sr ∷ ss ∷ st ∷ []) ∷ (st ∷ []) ∷ []
158 t-2 = Ntrace am2 LStates1 existsS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ [] ∷ [] 142 t-2 = Ntrace am2 LStates1 existsS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ [] ∷ []
159 t-3 = NtraceDepth am2 start1 LStates1 ( i1 ∷ i1 ∷ i1 ∷ [] ) 143 -- t-3 = NtraceDepth am2 start1 LStates1 ( i1 ∷ i1 ∷ i1 ∷ [] )
160 t-4 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ i0 ∷ [] ) 144 -- t-4 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ i0 ∷ [] )
161 t-5 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ [] ) 145 -- t-5 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ [] )
162 146
163 transition4 : States1 → In2 → States1 → Bool 147 transition4 : States1 → In2 → States1 → Bool
164 transition4 sr i0 sr = true 148 transition4 sr i0 sr = true
165 transition4 sr i1 ss = true 149 transition4 sr i1 ss = true
166 transition4 sr i1 sr = true 150 transition4 sr i1 sr = true