Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/nfa136.agda @ 408:3d0aa205edf9

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, 15 Nov 2023 16:24:07 +0900
parents 6f3636fbc481
children db02b6938e04
comparison
equal deleted inserted replaced
407:c7ad8d2dc157 408:3d0aa205edf9
43 43
44 example136-1 = Naccept nfa136 exists136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] ) 44 example136-1 = Naccept nfa136 exists136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] )
45 45
46 t146-1 = Ntrace nfa136 states136 exists136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] ) 46 t146-1 = Ntrace nfa136 states136 exists136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] )
47 47
48 test111 = ? 48 -- test111 = ?
49 49
50 example136-0 = Naccept nfa136 exists136 start136( a0 ∷ [] ) 50 example136-0 = Naccept nfa136 exists136 start136( a0 ∷ [] )
51 51
52 example136-2 = Naccept nfa136 exists136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] ) 52 example136-2 = Naccept nfa136 exists136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] )
53 t146-2 = Ntrace nfa136 states136 exists136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] ) 53 t146-2 = Ntrace nfa136 states136 exists136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] )
81 81
82 data Q2 : Set where 82 data Q2 : Set where
83 a0 : Q2 83 a0 : Q2
84 a1 : Q2 84 a1 : Q2
85 ae : Q2 85 ae : Q2
86 af : Q2
86 b0 : Q2 87 b0 : Q2
87 b1 : Q2 88 b1 : Q2
88 be : Q2 89 be : Q2
90 bf : Q2
89 91
90 -- a.*f 92 -- a.*f
91
92 aδ : Q2 → Σ2 → Q2 → Bool
93 aδ a0 ca a1 = true
94 aδ a0 _ _ = false
95 aδ a1 cf ae = true
96 aδ a1 _ a1 = true
97 aδ _ _ _ = false
98 93
99 a-end : Q2 → Bool 94 a-end : Q2 → Bool
100 a-end ae = true 95 a-end ae = true
101 a-end _ = false 96 a-end _ = false
102 97
98 aδ : Q2 → Σ2 → Q2
99 aδ a0 ca = a1
100 aδ a0 _ = af
101 aδ a1 cf = ae
102 aδ a1 _ = a1
103 aδ ae cf = ae
104 aδ ae _ = a1
105 aδ _ _ = af
106 fa-a : Automaton Q2 Σ2
107 fa-a = record { δ = aδ ; aend = a-end }
108
109 test111 : Bool
110 test111 = accept fa-a a0 ( ca ∷ cf ∷ ca ∷ [] )
111
112 b-end : Q2 → Bool
113 b-end be = true
114 b-end _ = false
115
116 bδ : Q2 → Σ2 → Q2
117 bδ b0 cb = b1
118 bδ b0 _ = bf
119 bδ b1 cf = be
120 bδ b1 _ = b1
121 bδ be cf = be
122 bδ be _ = b1
123 bδ _ _ = bf
124 fa-b : Automaton Q2 Σ2
125 fa-b = record { δ = bδ ; aend = b-end }
126
127 test115 : Bool
128 test115 = accept fa-b b0 ( cb ∷ cf ∷ cf ∷ [] )
129
130 open import regular-language
131
132 test116 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ cb ∷ cf ∷ cf ∷ [] )
133
134 naδ : Q2 → Σ2 → Q2 → Bool
135 naδ a0 ca a1 = true
136 naδ a0 _ _ = false
137 naδ a1 cf ae = true
138 naδ a1 _ a1 = true
139 naδ _ _ _ = false
140
103 a-start : Q2 → Bool 141 a-start : Q2 → Bool
104 a-start a0 = true 142 a-start a0 = true
105 a-start _ = false 143 a-start _ = false
106 144
107 nfa-a : NAutomaton Q2 Σ2 145 nfa-a : NAutomaton Q2 Σ2
108 nfa-a = record { Nδ = aδ ; Nend = a-end } 146 nfa-a = record { Nδ = naδ ; Nend = a-end }
109 147
110 nfa-a-exists : (Q2 → Bool) → Bool 148 nfa-a-exists : (Q2 → Bool) → Bool
111 nfa-a-exists p = p a0 \/ p a1 \/ p ae 149 nfa-a-exists p = p a0 \/ p a1 \/ p ae
112 150
113 test-a1 : Bool 151 test-a1 : Bool
114 test-a1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ [] ) 152 test-a1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ [] )
115 153
116 test-a2 = map reverse ( NtraceDepth nfa-a a-start (a0 ∷ a1 ∷ ae ∷ []) ( ca ∷ cf ∷ cf ∷ [] ) ) 154 -- test-a2 = map reverse ( NtraceDepth nfa-a a-start (a0 ∷ a1 ∷ ae ∷ []) ( ca ∷ cf ∷ cf ∷ [] ) )
117 155
118 -- b.*f 156 -- b.*f
119 157
120 bδ : Q2 → Σ2 → Q2 → Bool 158 nbδ : Q2 → Σ2 → Q2 → Bool
121 bδ ae cb b1 = true 159 nbδ ae cb b1 = true
122 bδ ae _ _ = false 160 nbδ ae _ _ = false
123 bδ b1 cf be = true 161 nbδ b1 cf be = true
124 bδ b1 _ b1 = true 162 nbδ b1 _ b1 = true
125 bδ _ _ _ = false 163 nbδ _ _ _ = false
126
127 b-end : Q2 → Bool
128 b-end be = true
129 b-end _ = false
130 164
131 b-start : Q2 → Bool 165 b-start : Q2 → Bool
132 b-start ae = true 166 b-start ae = true
133 b-start _ = false 167 b-start _ = false
134 168
135 nfa-b : NAutomaton Q2 Σ2 169 nfa-b : NAutomaton Q2 Σ2
136 nfa-b = record { Nδ = bδ ; Nend = b-end } 170 nfa-b = record { Nδ = nbδ ; Nend = b-end }
137 171
138 nfa-b-exists : (Q2 → Bool) → Bool 172 nfa-b-exists : (Q2 → Bool) → Bool
139 nfa-b-exists p = p b0 \/ p b1 \/ p ae 173 nfa-b-exists p = p b0 \/ p b1 \/ p ae
140 174
141 -- (a.*f)(b.*f) 175 -- (a.*f)(b.*f)
142 176
143 abδ : Q2 → Σ2 → Q2 → Bool 177 abδ : Q2 → Σ2 → Q2 → Bool
144 abδ x i y = aδ x i y \/ bδ x i y 178 abδ x i y = naδ x i y \/ nbδ x i y
145 179
146 nfa-ab : NAutomaton Q2 Σ2 180 nfa-ab : NAutomaton Q2 Σ2
147 nfa-ab = record { Nδ = abδ ; Nend = b-end } 181 nfa-ab = record { Nδ = abδ ; Nend = b-end }
148 182
149 nfa-ab-exists : (Q2 → Bool) → Bool 183 nfa-ab-exists : (Q2 → Bool) → Bool
153 test-ab1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ) 187 test-ab1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )
154 188
155 test-ab2 : Bool 189 test-ab2 : Bool
156 test-ab2 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] ) 190 test-ab2 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
157 191
158 test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae ∷ b0 ∷ b1 ∷ be ∷ []) ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )) 192 -- test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae ∷ b0 ∷ b1 ∷ be ∷ []) ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ))
159 193
160 test112 : Automaton (Q2 → Bool) Σ2 194 test112 : Automaton (Q2 → Bool) Σ2
161 test112 = subset-construction nfa-ab-exists nfa-ab 195 test112 = subset-construction nfa-ab-exists nfa-ab
162 196
163 test114 = Automaton.δ (subset-construction nfa-ab-exists nfa-ab) 197 test114 = Automaton.δ (subset-construction nfa-ab-exists nfa-ab)
164 198
165 test113 : Bool 199 test113 : Bool
166 test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] ) 200 test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
167 201
202 --
203
204
205
206
207
208