Mercurial > hg > Members > kono > Proof > automaton

annotate automaton-in-agda/src/automaton.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/automaton.agda@567754463810
children 91781b7c65a8
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module automaton where
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
3 open import Data.Nat
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
4 open import Data.List
58
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
5 open import Relation.Binary.PropositionalEquality hiding ( [_] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
6 open import logic
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
8 record Automaton ( Q : Set ) ( Σ : Set )
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 : Set where
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
10 field
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
11 δ : Q → Σ → Q
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
12 aend : Q → Bool
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
13
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
14 open Automaton
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
16 accept : { Q : Set } { Σ : Set }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
17 → Automaton Q Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
18 → (astart : Q)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
19 → List Σ → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
20 accept {Q} { Σ} M q [] = aend M q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
21 accept {Q} { Σ} M q ( H ∷ T ) = accept M ( (δ M) q H ) T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
22
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
23 moves : { Q : Set } { Σ : Set }
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
24 → Automaton Q Σ
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 → Q → List Σ → Q
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
26 moves {Q} { Σ} M q [] = q
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
27 moves {Q} { Σ} M q ( H ∷ T ) = moves M ( δ M q H) T
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
29 trace : { Q : Set } { Σ : Set }
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
30 → Automaton Q Σ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
31 → Q → List Σ → List Q
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
32 trace {Q} { Σ} M q [] = q ∷ []
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
33 trace {Q} { Σ} M q ( H ∷ T ) = q ∷ trace M ( (δ M) q H ) T
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
35 reachable : { Q : Set } { Σ : Set }
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
36 → (M : Automaton Q Σ )
60
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
37 → (astart q : Q )
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
38 → (L : List Σ ) → Set
60
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
39 reachable M astart q L = moves M astart L ≡ q
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40