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