Mercurial > hg > Members > kono > Proof > automaton

annotate automaton-in-agda/src/automaton-ex.agda @ 205:e97cf4fb67fa

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 Fri, 18 Jun 2021 21:09:50 +0900
parents 3fa72793620b
children e5cf49902db3
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module automaton-ex where
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.Nat
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.List
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Maybe
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Relation.Binary.PropositionalEquality hiding ( [_] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Relation.Nullary using (¬_; Dec; yes; no)
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import logic
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import automaton
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open Automaton
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 data StatesQ : Set where
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 q1 : StatesQ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 q2 : StatesQ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 q3 : StatesQ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 data In2 : Set where
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 i0 : In2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 i1 : In2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 transitionQ : StatesQ → In2 → StatesQ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 transitionQ q1 i0 = q1
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 transitionQ q1 i1 = q2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 transitionQ q2 i0 = q3
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 transitionQ q2 i1 = q2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 transitionQ q3 i0 = q2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 transitionQ q3 i1 = q2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 aendQ : StatesQ → Bool
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 aendQ q2 = true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 aendQ _ = false
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 a1 : Automaton StatesQ In2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 a1 = record {
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 δ = transitionQ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 ; aend = aendQ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 }
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 test1 : accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ false
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 test1 = refl
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 test2 = accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 data States1 : Set where
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 sr : States1
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 ss : States1
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 st : States1
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 transition1 : States1 → In2 → States1
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 transition1 sr i0 = sr
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 transition1 sr i1 = ss
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 transition1 ss i0 = sr
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 transition1 ss i1 = st
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 transition1 st i0 = sr
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 transition1 st i1 = st
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 fin1 : States1 → Bool
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 fin1 st = true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 fin1 ss = false
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 fin1 sr = false
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 am1 : Automaton States1 In2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 am1 = record { δ = transition1 ; aend = fin1 }
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 example1-1 = accept am1 sr ( i0 ∷ i1 ∷ i0 ∷ [] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 example1-2 = accept am1 sr ( i1 ∷ i1 ∷ i1 ∷ [] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 trace-2 = trace am1 sr ( i1 ∷ i1 ∷ i1 ∷ [] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 example1-3 = reachable am1 sr st ( i1 ∷ i1 ∷ i1 ∷ [] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 ieq : (i i' : In2 ) → Dec ( i ≡ i' )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 ieq i0 i0 = yes refl
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 ieq i1 i1 = yes refl
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 ieq i0 i1 = no ( λ () )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 ieq i1 i0 = no ( λ () )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76