Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/nfa.agda @ 183:3fa72793620b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Jun 2021 20:45:17 +0900
parents automaton-in-agda/src/agda/nfa.agda@567754463810
children ae70f96cb60c
comparison
equal deleted inserted replaced
182:567754463810 183:3fa72793620b
1 {-# OPTIONS --allow-unsolved-metas #-}
2 module nfa where
3
4 -- open import Level renaming ( suc to succ ; zero to Zero )
5 open import Data.Nat
6 open import Data.List
7 open import Data.Fin hiding ( _<_ )
8 open import Data.Maybe
9 open import Relation.Nullary
10 open import Data.Empty
11 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
13 open import Relation.Nullary using (¬_; Dec; yes; no)
14 open import logic
15
16 data States1 : Set where
17 sr : States1
18 ss : States1
19 st : States1
20
21 data In2 : Set where
22 i0 : In2
23 i1 : In2
24
25
26 record NAutomaton ( Q : Set ) ( Σ : Set )
27 : Set where
28 field
29 Nδ : Q → Σ → Q → Bool
30 Nend : Q → Bool
31
32 open NAutomaton
33
34 LStates1 : List States1
35 LStates1 = sr ∷ ss ∷ st ∷ []
36
37 -- one of qs q is true
38 existsS1 : ( States1 → Bool ) → Bool
39 existsS1 qs = qs sr \/ qs ss \/ qs st
40
41 -- extract list of q which qs q is true
42 to-listS1 : ( States1 → Bool ) → List States1
43 to-listS1 qs = ss1 LStates1 where
44 ss1 : List States1 → List States1
45 ss1 [] = []
46 ss1 (x ∷ t) with qs x
47 ... | true = x ∷ ss1 t
48 ... | false = ss1 t
49
50 Nmoves : { Q : Set } { Σ : Set }
51 → NAutomaton Q Σ
52 → (exists : ( Q → Bool ) → Bool)
53 → ( Qs : Q → Bool ) → (s : Σ ) → Q → Bool
54 Nmoves {Q} { Σ} M exists Qs s q =
55 exists ( λ qn → (Qs qn /\ ( Nδ M qn s q ) ))
56
57 Naccept : { Q : Set } { Σ : Set }
58 → NAutomaton Q Σ
59 → (exists : ( Q → Bool ) → Bool)
60 → (Nstart : Q → Bool) → List Σ → Bool
61 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
63
64 Ntrace : { Q : Set } { Σ : Set }
65 → NAutomaton Q Σ
66 → (exists : ( Q → Bool ) → Bool)
67 → (to-list : ( Q → Bool ) → List Q )
68 → (Nstart : Q → Bool) → List Σ → List (List Q)
69 Ntrace M exists to-list sb [] = to-list ( λ q → sb q /\ Nend M q ) ∷ []
70 Ntrace M exists to-list sb (i ∷ t ) =
71 to-list (λ q → sb q ) ∷
72 Ntrace M exists to-list (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t
73
74
75 transition3 : States1 → In2 → States1 → Bool
76 transition3 sr i0 sr = true
77 transition3 sr i1 ss = true
78 transition3 sr i1 sr = true
79 transition3 ss i0 sr = true
80 transition3 ss i1 st = true
81 transition3 st i0 sr = true
82 transition3 st i1 st = true
83 transition3 _ _ _ = false
84
85 fin1 : States1 → Bool
86 fin1 st = true
87 fin1 ss = false
88 fin1 sr = false
89
90 test5 = existsS1 (λ q → fin1 q )
91 test6 = to-listS1 (λ q → fin1 q )
92
93 start1 : States1 → Bool
94 start1 sr = true
95 start1 _ = false
96
97 am2 : NAutomaton States1 In2
98 am2 = record { Nδ = transition3 ; Nend = fin1}
99
100 example2-1 = Naccept am2 existsS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] )
101 example2-2 = Naccept am2 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] )
102
103 t-1 : List ( List States1 )
104 t-1 = Ntrace am2 existsS1 to-listS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] )
105 t-2 = Ntrace am2 existsS1 to-listS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] )
106
107 transition4 : States1 → In2 → States1 → Bool
108 transition4 sr i0 sr = true
109 transition4 sr i1 ss = true
110 transition4 sr i1 sr = true
111 transition4 ss i0 ss = true
112 transition4 ss i1 st = true
113 transition4 st i0 st = true
114 transition4 st i1 st = true
115 transition4 _ _ _ = false
116
117 fin4 : States1 → Bool
118 fin4 st = true
119 fin4 _ = false
120
121 start4 : States1 → Bool
122 start4 ss = true
123 start4 _ = false
124
125 am4 : NAutomaton States1 In2
126 am4 = record { Nδ = transition4 ; Nend = fin4}
127
128 example4-1 = Naccept am4 existsS1 start4 ( i0 ∷ i1 ∷ i1 ∷ i0 ∷ [] )
129 example4-2 = Naccept am4 existsS1 start4 ( i0 ∷ i1 ∷ i1 ∷ i1 ∷ [] )
130
131 fin0 : States1 → Bool
132 fin0 st = false
133 fin0 ss = false
134 fin0 sr = false
135
136 test0 : Bool
137 test0 = existsS1 fin0
138
139 test1 : Bool
140 test1 = existsS1 fin1
141
142 test2 = Nmoves am2 existsS1 start1
143
144 open import automaton
145
146 am2def : Automaton (States1 → Bool ) In2
147 am2def = record { δ = λ qs s q → existsS1 (λ qn → qs q /\ Nδ am2 q s qn )
148 ; aend = λ qs → existsS1 (λ q → qs q /\ Nend am2 q) }
149
150 dexample4-1 = accept am2def start1 ( i0 ∷ i1 ∷ i1 ∷ i0 ∷ [] )
151 texample4-1 = trace am2def start1 ( i0 ∷ i1 ∷ i1 ∷ i0 ∷ [] )
152