Mercurial > hg > Members > kono > Proof > automaton

annotate automaton-in-agda/src/automaton.agda @ 403:c298981108c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix for std-lib 2.0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 11:32:01 +0900
parents 91781b7c65a8
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
403
c298981108c1 fix for std-lib 2.0
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 318
diff changeset
1 {-# OPTIONS --cubical-compatible --safe #-}
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 module automaton where
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
4 open import Data.Nat
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
5 open import Data.List
58
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
6 open import Relation.Binary.PropositionalEquality hiding ( [_] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
7 open import logic
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
9 record Automaton ( Q : Set ) ( Σ : Set )
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 : Set where
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
11 field
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
12 δ : Q → Σ → Q
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
13 aend : Q → Bool
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
14
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
15 open Automaton
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
17 accept : { Q : Set } { Σ : Set }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
18 → Automaton Q Σ
318
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
19 → Q
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
20 → List Σ → Bool
318
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
21 accept M q [] = aend M q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
22 accept M q ( H ∷ T ) = accept M ( δ M q H ) T
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 64
diff changeset
23
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
24 moves : { Q : Set } { Σ : Set }
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
25 → Automaton Q Σ
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 → Q → List Σ → Q
318
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
27 moves M q [] = q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
28 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
29
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
30 trace : { Q : Set } { Σ : Set }
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
31 → Automaton Q Σ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
32 → Q → List Σ → List Q
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
33 trace {Q} { Σ} M q [] = q ∷ []
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 67
diff changeset
34 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
35
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
36 reachable : { Q : Set } { Σ : Set }
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
37 → (M : Automaton Q Σ )
60
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
38 → (astart q : Q )
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
39 → (L : List Σ ) → Set
60
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
40 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
41