Mercurial > hg > Members > kono > Proof > automaton

changeset 60:64ea7d12894c

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, 24 Oct 2019 12:20:34 +0900
parents 25977ccee101
children 6d50a933bcb3
files agda/automaton.agda
diffstat 1 files changed, 8 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/agda/automaton.agda	Wed Oct 23 19:21:16 2019 +0900
+++ b/agda/automaton.agda	Thu Oct 24 12:20:34 2019 +0900
@@ -13,7 +13,6 @@
        : Set  where
     field
         δ : Q → Σ → Q
-        astart : Q
         aend : Q → Bool
 
 open Automaton
@@ -38,8 +37,9 @@
 
 accept : { Q : Set } { Σ : Set  }
     → Automaton Q  Σ
+    → (astart : Q)
     → List  Σ → Bool
-accept {Q} { Σ} M L = move (astart M) L
+accept {Q} { Σ} M astart L = move astart L
    where
       move : (q : Q ) ( L : List  Σ ) → Bool
       move q [] = aend M q
@@ -59,19 +59,19 @@
 fin1 sr = false
 
 am1  :  Automaton  States1 In2
-am1  =  record {  δ = transition1 ; astart = sr ; aend = fin1   }
+am1  =  record {  δ = transition1 ; aend = fin1   }
 
 
-example1-1 = accept am1 ( i0  ∷ i1  ∷ i0  ∷ [] )
-example1-2 = accept am1 ( i1  ∷ i1  ∷ i1  ∷ [] )
+example1-1 = accept am1 sr ( i0  ∷ i1  ∷ i0  ∷ [] )
+example1-2 = accept am1 sr ( i1  ∷ i1  ∷ i1  ∷ [] )
 
 reachable : { Q : Set } { Σ : Set  }
     → (M : Automaton Q  Σ  )
-    → (q : Q )
+    → (astart q : Q )
     → (L : List  Σ ) → Set
-reachable M q L = moves M (astart M)  L ≡ q
+reachable M astart q L = moves M astart  L ≡ q
 
-example1-3 = reachable am1 st ( i1  ∷ i1  ∷ i1  ∷ [] )
+example1-3 = reachable am1 sr st ( i1  ∷ i1  ∷ i1  ∷ [] )
 
 ieq : (i i' : In2 ) → Dec ( i ≡ i' )
 ieq i0 i0 = yes refl