Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/nfa136.agda @ 410:db02b6938e04

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
StarProp and Ntrace
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 22 Nov 2023 17:07:01 +0900
parents 3d0aa205edf9
children
comparison
equal deleted inserted replaced
409:4e4acdc43dee 410:db02b6938e04
95 a-end ae = true 95 a-end ae = true
96 a-end _ = false 96 a-end _ = false
97 97
98 aδ : Q2 → Σ2 → Q2 98 aδ : Q2 → Σ2 → Q2
99 aδ a0 ca = a1 99 aδ a0 ca = a1
100 aδ a0 _ = af 100 aδ a0 cb = af
101 aδ a0 cc = af
102 aδ a0 cf = af
101 aδ a1 cf = ae 103 aδ a1 cf = ae
102 aδ a1 _ = a1 104 aδ a1 _ = a1
103 aδ ae cf = ae 105 aδ ae cf = ae
104 aδ ae _ = a1 106 aδ ae _ = a1
105 aδ _ _ = af 107 aδ _ _ = af
107 fa-a = record { δ = aδ ; aend = a-end } 109 fa-a = record { δ = aδ ; aend = a-end }
108 110
109 test111 : Bool 111 test111 : Bool
110 test111 = accept fa-a a0 ( ca ∷ cf ∷ ca ∷ [] ) 112 test111 = accept fa-a a0 ( ca ∷ cf ∷ ca ∷ [] )
111 113
114 -- b.*f
115
112 b-end : Q2 → Bool 116 b-end : Q2 → Bool
113 b-end be = true 117 b-end be = true
114 b-end _ = false 118 b-end _ = false
115 119
116 bδ : Q2 → Σ2 → Q2 120 bδ : Q2 → Σ2 → Q2
117 bδ b0 cb = b1 121 bδ ae cb = b1
118 bδ b0 _ = bf 122 bδ ae _ = bf
119 bδ b1 cf = be 123 bδ b1 cf = be
120 bδ b1 _ = b1 124 bδ b1 _ = b1
121 bδ be cf = be 125 bδ be cf = be
122 bδ be _ = b1 126 bδ be _ = b1
123 bδ _ _ = bf 127 bδ _ _ = bf
127 test115 : Bool 131 test115 : Bool
128 test115 = accept fa-b b0 ( cb ∷ cf ∷ cf ∷ [] ) 132 test115 = accept fa-b b0 ( cb ∷ cf ∷ cf ∷ [] )
129 133
130 open import regular-language 134 open import regular-language
131 135
136 -- (a.*f)(b.*f) -- a.*(fb).*f
132 test116 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ cb ∷ cf ∷ cf ∷ [] ) 137 test116 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ cb ∷ cf ∷ cf ∷ [] )
138 -- a0 ae b0 b1 be
139 test117 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ ca ∷ cb ∷ ca ∷ cf ∷ cf ∷ [] )
140 -- a0 ae a0 b0 b1 be
141 -- a0 ae ae b0 b1 be
133 142
134 naδ : Q2 → Σ2 → Q2 → Bool 143 naδ : Q2 → Σ2 → Q2 → Bool
135 naδ a0 ca a1 = true 144 naδ a0 ca a1 = true
136 naδ a0 _ _ = false 145 naδ a0 _ _ = false
137 naδ a1 cf ae = true 146 naδ a1 cf ae = true
138 naδ a1 _ a1 = true 147 naδ a1 _ a1 = true
148 naδ ae cf ae = true
149 naδ ae _ a1 = true
139 naδ _ _ _ = false 150 naδ _ _ _ = false
140 151
141 a-start : Q2 → Bool 152 a-start : Q2 → Bool
142 a-start a0 = true 153 a-start a0 = true
143 a-start _ = false 154 a-start _ = false
158 nbδ : Q2 → Σ2 → Q2 → Bool 169 nbδ : Q2 → Σ2 → Q2 → Bool
159 nbδ ae cb b1 = true 170 nbδ ae cb b1 = true
160 nbδ ae _ _ = false 171 nbδ ae _ _ = false
161 nbδ b1 cf be = true 172 nbδ b1 cf be = true
162 nbδ b1 _ b1 = true 173 nbδ b1 _ b1 = true
174 nbδ be cf be = true
175 nbδ be _ b1 = true
163 nbδ _ _ _ = false 176 nbδ _ _ _ = false
164 177
165 b-start : Q2 → Bool 178 b-start : Q2 → Bool
166 b-start ae = true 179 b-start ae = true
167 b-start _ = false 180 b-start _ = false
168 181
169 nfa-b : NAutomaton Q2 Σ2 182 nfa-b : NAutomaton Q2 Σ2
170 nfa-b = record { Nδ = nbδ ; Nend = b-end } 183 nfa-b = record { Nδ = nbδ ; Nend = b-end }
171 184
172 nfa-b-exists : (Q2 → Bool) → Bool 185 nfa-b-exists : (Q2 → Bool) → Bool
173 nfa-b-exists p = p b0 \/ p b1 \/ p ae 186 nfa-b-exists p = p b0 \/ p b1 \/ p be
174 187
175 -- (a.*f)(b.*f) 188 -- (a.*f)(b.*f)
176 189
177 abδ : Q2 → Σ2 → Q2 → Bool 190 abδ : Q2 → Σ2 → Q2 → Bool
178 abδ x i y = naδ x i y \/ nbδ x i y 191 abδ x i y = naδ x i y \/ nbδ x i y
181 nfa-ab = record { Nδ = abδ ; Nend = b-end } 194 nfa-ab = record { Nδ = abδ ; Nend = b-end }
182 195
183 nfa-ab-exists : (Q2 → Bool) → Bool 196 nfa-ab-exists : (Q2 → Bool) → Bool
184 nfa-ab-exists p = nfa-a-exists p \/ nfa-b-exists p 197 nfa-ab-exists p = nfa-a-exists p \/ nfa-b-exists p
185 198
199 test-ab1-data : List Σ2
200 test-ab1-data = ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )
201
186 test-ab1 : Bool 202 test-ab1 : Bool
187 test-ab1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ) 203 test-ab1 = Naccept nfa-ab nfa-ab-exists a-start test-ab1-data -- should be false
204
205 test-ab2-data : List Σ2
206 test-ab2-data = ( ca ∷ cf ∷ ca ∷ cf ∷ cb ∷ cb ∷ cf ∷ [] )
188 207
189 test-ab2 : Bool 208 test-ab2 : Bool
190 test-ab2 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] ) 209 test-ab2 = Naccept nfa-ab nfa-ab-exists a-start test-ab2-data -- should be true
210
211 q2-list : List Q2
212 q2-list = a0 ∷ a1 ∷ ae ∷ af ∷ b0 ∷ b1 ∷ be ∷ bf ∷ []
213
214 test-tr : List (List Q2)
215 test-tr = Ntrace nfa-ab q2-list nfa-ab-exists a-start ( ca ∷ cf ∷ cf ∷ cb ∷ cb ∷ cf ∷ [] )
191 216
192 -- test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae ∷ b0 ∷ b1 ∷ be ∷ []) ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )) 217 -- test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae ∷ b0 ∷ b1 ∷ be ∷ []) ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ))
193 218
194 test112 : Automaton (Q2 → Bool) Σ2 219 test112 : Automaton (Q2 → Bool) Σ2
195 test112 = subset-construction nfa-ab-exists nfa-ab 220 test112 = subset-construction nfa-ab-exists nfa-ab
198 223
199 test113 : Bool 224 test113 : Bool
200 test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] ) 225 test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
201 226
202 -- 227 --
203 228 open import regex
204 229 open import Relation.Nullary using (¬_; Dec; yes; no)
205 230
206 231 Σ2-cmp : (x y : Σ2 ) → Dec (x ≡ y)
207 232 Σ2-cmp ca ca = yes refl
208 233 Σ2-cmp ca cb = no (λ ())
234 Σ2-cmp ca cc = no (λ ())
235 Σ2-cmp ca cf = no (λ ())
236 Σ2-cmp cb ca = no (λ ())
237 Σ2-cmp cb cb = yes refl
238 Σ2-cmp cb cc = no (λ ())
239 Σ2-cmp cb cf = no (λ ())
240 Σ2-cmp cc ca = no (λ ())
241 Σ2-cmp cc cb = no (λ ())
242 Σ2-cmp cc cc = yes refl
243 Σ2-cmp cc cf = no (λ ())
244 Σ2-cmp cf ca = no (λ ())
245 Σ2-cmp cf cb = no (λ ())
246 Σ2-cmp cf cc = no (λ ())
247 Σ2-cmp cf cf = yes refl
248
249 Σ2-any : Regex Σ2
250 Σ2-any = < ca > || < cb > || < cc > || < cf >
251
252 test-ab1-regex : regex-language ( (< ca > & (Σ2-any *) & < cf > ) & (< cb > & (Σ2-any *) & < cf > ) ) Σ2-cmp test-ab1-data ≡ false
253 test-ab1-regex = refl
254
255 test-ab2-regex : regex-language ( (< ca > & (Σ2-any *) & < cf > ) & (< cb > & (Σ2-any *) & < cf > ) ) Σ2-cmp test-ab2-data ≡ true
256 test-ab2-regex = refl
257
258
259
260