Mercurial > hg > Members > kono > Proof > automaton

annotate automaton-in-agda/src/automaton.agda @ 395:cd81e0869fac

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 Thu, 03 Aug 2023 14:55:14 +0900
parents 91781b7c65a8
children c298981108c1
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 Σ
318
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
18 → Q
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
19 → List Σ → Bool
318
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
20 accept M q [] = aend M q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
21 accept M q ( H ∷ T ) = accept M ( δ M q H ) T
65
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
318
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
26 moves M q [] = q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
27 moves 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