Mercurial > hg > Members > kono > Proof > automaton

comparison agda/nfa136.agda @ 104:fba1cd54581d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use exists in cond, nfa example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 14 Nov 2019 05:13:49 +0900
parents
children b3f05cd08d24
comparison
equal deleted inserted replaced
103:a46e0a2a3543 104:fba1cd54581d
1 module nfa136 where
2
3 open import logic
4 open import nfa
5 open import automaton hiding ( StatesQ )
6 open import Data.List
7 open import finiteSet
8 open import Data.Fin
9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
10
11 data StatesQ : Set where
12 q1 : StatesQ
13 q2 : StatesQ
14 q3 : StatesQ
15
16 data A2 : Set where
17 a0 : A2
18 b0 : A2
19
20 finStateQ : FiniteSet StatesQ
21 finStateQ = record {
22 Q←F = Q←F
23 ; F←Q = F←Q
24 ; finiso→ = finiso→
25 ; finiso← = finiso←
26 } where
27 Q←F : Fin 3 → StatesQ
28 Q←F zero = q1
29 Q←F (suc zero) = q2
30 Q←F (suc (suc zero)) = q3
31 F←Q : StatesQ → Fin 3
32 F←Q q1 = zero
33 F←Q q2 = suc zero
34 F←Q q3 = suc (suc zero)
35 finiso→ : (q : StatesQ) → Q←F (F←Q q) ≡ q
36 finiso→ q1 = refl
37 finiso→ q2 = refl
38 finiso→ q3 = refl
39 finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f
40 finiso← zero = refl
41 finiso← (suc zero) = refl
42 finiso← (suc (suc zero)) = refl
43 finiso← (suc (suc (suc ())))
44
45 transition136 : StatesQ → A2 → StatesQ → Bool
46 transition136 q1 b0 q2 = true
47 transition136 q1 a0 q1 = true -- q1 → ep → q3
48 transition136 q2 a0 q2 = true
49 transition136 q2 a0 q3 = true
50 transition136 q2 b0 q3 = true
51 transition136 q3 a0 q1 = true
52 transition136 _ _ _ = false
53
54 end136 : StatesQ → Bool
55 end136 q1 = true
56 end136 _ = false
57
58 start136 : StatesQ → Bool
59 start136 q1 = true
60 start136 _ = false
61
62 nfa136 : NAutomaton StatesQ A2
63 nfa136 = record { Nδ = transition136; Nend = end136 }
64
65 example136-1 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] )
66
67 example136-0 = Naccept nfa136 finStateQ start136( a0 ∷ [] )
68
69 example136-2 = Naccept nfa136 finStateQ start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] )
70
71 open FiniteSet
72
73 nx : (StatesQ → Bool) → (List A2 ) → StatesQ → Bool
74 nx now [] = now
75 nx now ( i ∷ ni ) = (Nmoves nfa136 finStateQ (nx now ni) i )
76
77 example136-3 = to-list finStateQ start136
78 example136-4 = to-list finStateQ (nx start136 ( a0 ∷ b0 ∷ a0 ∷ [] ))
79
80 open import sbconst2
81
82 fm136 : Automaton ( StatesQ → Bool ) A2
83 -- fm136 = record { δ = λ qs q → transition136 {!!} {!!} ; aend = λ qs → exists finStateQ end136 }
84 fm136 = subset-construction finStateQ nfa136 q1
85
86 open NAutomaton
87
88 lemma136 : ( x : List A2 ) → Naccept nfa136 finStateQ start136 x ≡ accept fm136 start136 x
89 lemma136 x = lemma136-1 x start136 where
90 lemma136-1 : ( x : List A2 ) → ( states : StatesQ → Bool )
91 → Naccept nfa136 finStateQ states x ≡ accept fm136 states x
92 lemma136-1 [] _ = refl
93 lemma136-1 (h ∷ t) states = lemma136-1 t (δconv finStateQ (Nδ nfa136) states h)