|
405
|
1 {-# OPTIONS --cubical-compatible --safe #-}
|
|
|
2
|
|
141
|
3 module automaton-ex where
|
|
|
4
|
|
|
5 open import Data.Nat
|
|
|
6 open import Data.List
|
|
|
7 open import Data.Maybe
|
|
|
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
266
|
9 open import Relation.Binary.Definitions
|
|
141
|
10 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
|
11 open import logic
|
|
|
12
|
|
|
13 open import automaton
|
|
|
14 open Automaton
|
|
|
15
|
|
|
16 data StatesQ : Set where
|
|
|
17 q1 : StatesQ
|
|
|
18 q2 : StatesQ
|
|
|
19 q3 : StatesQ
|
|
|
20
|
|
|
21 data In2 : Set where
|
|
|
22 i0 : In2
|
|
|
23 i1 : In2
|
|
266
|
24
|
|
|
25 transitionQ : StatesQ → In2 → StatesQ
|
|
141
|
26 transitionQ q1 i0 = q1
|
|
|
27 transitionQ q1 i1 = q2
|
|
|
28 transitionQ q2 i0 = q3
|
|
|
29 transitionQ q2 i1 = q2
|
|
|
30 transitionQ q3 i0 = q2
|
|
|
31 transitionQ q3 i1 = q2
|
|
|
32
|
|
|
33 aendQ : StatesQ → Bool
|
|
330
|
34 aendQ q1 = false
|
|
141
|
35 aendQ q2 = true
|
|
330
|
36 aendQ q3 = false
|
|
141
|
37
|
|
|
38 a1 : Automaton StatesQ In2
|
|
|
39 a1 = record {
|
|
|
40 δ = transitionQ
|
|
|
41 ; aend = aendQ
|
|
|
42 }
|
|
|
43
|
|
|
44 test1 : accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ false
|
|
|
45 test1 = refl
|
|
|
46 test2 = accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] )
|
|
266
|
47 test3 = trace a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] )
|
|
141
|
48
|
|
|
49 data States1 : Set where
|
|
|
50 sr : States1
|
|
|
51 ss : States1
|
|
|
52 st : States1
|
|
|
53
|
|
|
54 transition1 : States1 → In2 → States1
|
|
|
55 transition1 sr i0 = sr
|
|
|
56 transition1 sr i1 = ss
|
|
|
57 transition1 ss i0 = sr
|
|
|
58 transition1 ss i1 = st
|
|
|
59 transition1 st i0 = sr
|
|
|
60 transition1 st i1 = st
|
|
|
61
|
|
|
62 fin1 : States1 → Bool
|
|
|
63 fin1 st = true
|
|
|
64 fin1 ss = false
|
|
|
65 fin1 sr = false
|
|
|
66
|
|
|
67 am1 : Automaton States1 In2
|
|
|
68 am1 = record { δ = transition1 ; aend = fin1 }
|
|
|
69
|
|
|
70
|
|
|
71 example1-1 = accept am1 sr ( i0 ∷ i1 ∷ i0 ∷ [] )
|
|
|
72 example1-2 = accept am1 sr ( i1 ∷ i1 ∷ i1 ∷ [] )
|
|
|
73 trace-2 = trace am1 sr ( i1 ∷ i1 ∷ i1 ∷ [] )
|
|
|
74
|
|
|
75 example1-3 = reachable am1 sr st ( i1 ∷ i1 ∷ i1 ∷ [] )
|
|
|
76
|
|
266
|
77 -- data Dec' (A : Set) : Set where
|
|
|
78 -- yes' : A → Dec' A
|
|
|
79 -- no' : ¬ A → Dec' A
|
|
|
80 --
|
|
|
81 -- ieq' : (i i' : In2 ) → Dec' ( i ≡ i' )
|
|
|
82 -- ieq' i0 i0 = yes' refl
|
|
|
83 -- ieq' i1 i1 = yes' refl
|
|
|
84 -- ieq' i0 i1 = no' ( λ () )
|
|
|
85 -- ieq' i1 i0 = no' ( λ () )
|
|
|
86
|
|
141
|
87 ieq : (i i' : In2 ) → Dec ( i ≡ i' )
|
|
|
88 ieq i0 i0 = yes refl
|
|
|
89 ieq i1 i1 = yes refl
|
|
|
90 ieq i0 i1 = no ( λ () )
|
|
|
91 ieq i1 i0 = no ( λ () )
|
|
|
92
|
|
266
|
93 -- p.83 problem 1.4
|
|
|
94 --
|
|
|
95 -- w has at least three i0's and at least two i1's
|
|
|
96
|
|
|
97 count-chars : List In2 → In2 → ℕ
|
|
|
98 count-chars [] _ = 0
|
|
|
99 count-chars (h ∷ t) x with ieq h x
|
|
|
100 ... | yes y = suc ( count-chars t x )
|
|
|
101 ... | no n = count-chars t x
|
|
|
102
|
|
|
103 test11 : count-chars ( i1 ∷ i1 ∷ i0 ∷ [] ) i0 ≡ 1
|
|
|
104 test11 = refl
|
|
|
105
|
|
405
|
106 _≥b_ : ( x y : ℕ) → Bool
|
|
|
107 x ≥b y with <-cmp x y
|
|
|
108 ... | tri< a ¬b ¬c = false
|
|
|
109 ... | tri≈ ¬a b ¬c = true
|
|
|
110 ... | tri> ¬a ¬b c = true
|
|
|
111
|
|
|
112 _>b_ : ( x y : ℕ) → Bool
|
|
|
113 x >b y with <-cmp x y
|
|
|
114 ... | tri< a ¬b ¬c = false
|
|
|
115 ... | tri≈ ¬a b ¬c = false
|
|
|
116 ... | tri> ¬a ¬b c = true
|
|
|
117
|
|
|
118 _≤b_ : ( x y : ℕ) → Bool
|
|
|
119 x ≤b y = y ≥b x
|
|
|
120
|
|
|
121 _<b_ : ( x y : ℕ) → Bool
|
|
|
122 x <b y = y >b x
|
|
|
123
|
|
266
|
124 ex1_4a : (x : List In2) → Bool
|
|
|
125 ex1_4a x = ( count-chars x i0 ≥b 3 ) /\ ( count-chars x i1 ≥b 2 )
|
|
|
126
|
|
|
127 language' : { Σ : Set } → Set
|
|
|
128 language' {Σ} = List Σ → Bool
|
|
|
129
|
|
|
130 lang14a : language' {In2}
|
|
|
131 lang14a = ex1_4a
|
|
|
132
|
|
|
133 open _∧_
|
|
|
134
|
|
|
135 am14a-tr : ℕ ∧ ℕ → In2 → ℕ ∧ ℕ
|
|
|
136 am14a-tr p i0 = record { proj1 = suc (proj1 p) ; proj2 = proj2 p }
|
|
|
137 am14a-tr p i1 = record { proj1 = proj1 p ; proj2 = suc (proj2 p) }
|
|
|
138
|
|
|
139 am14a : Automaton (ℕ ∧ ℕ) In2
|
|
|
140 am14a = record { δ = am14a-tr ; aend = λ x → ( proj1 x ≥b 3 ) /\ ( proj2 x ≥b 2 )}
|
|
|
141
|
|
|
142 data am14s : Set where
|
|
|
143 a00 : am14s
|
|
|
144 a10 : am14s
|
|
|
145 a20 : am14s
|
|
|
146 a30 : am14s
|
|
|
147 a01 : am14s
|
|
|
148 a11 : am14s
|
|
|
149 a21 : am14s
|
|
|
150 a31 : am14s
|
|
|
151 a02 : am14s
|
|
|
152 a12 : am14s
|
|
|
153 a22 : am14s
|
|
|
154 a32 : am14s
|
|
|
155
|
|
|
156 am14a-tr' : am14s → In2 → am14s
|
|
|
157 am14a-tr' a00 i0 = a10
|
|
|
158 am14a-tr' _ _ = a10
|
|
|
159
|
|
405
|
160 -- am14a' : Automaton am14s In2
|
|
|
161 -- am14a' = record { δ = am14a-tr' ; aend = λ x → {!!} }
|
