Mercurial > hg > Members > kono > Proof > automaton

changeset 140:4c3fbfde1bc2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
utm tester
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Mar 2020 19:42:27 +0900
parents 3be1afb87f82
children b3f05cd08d24
files agda/utm.agda
diffstat 1 files changed, 22 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/agda/utm.agda	Sat Mar 14 17:34:54 2020 +0900
+++ b/agda/utm.agda	Sat Mar 14 19:42:27 2020 +0900
@@ -7,6 +7,7 @@
 open import Data.Nat
 
 data utmStates : Set where
+     reads : utmStates
      read0 : utmStates
      read1 : utmStates
      read2 : utmStates
@@ -67,6 +68,7 @@
     b : utmΣ
 
 utmδ :  utmStates →  utmΣ  → utmStates × (Write utmΣ) × Move
+utmδ reads  x = read0 , wnone , mnone
 utmδ read0  * = read1 , write * , left
 utmδ read0  x = read0 , write x , right
 utmδ read1  x = read2 , write ＠ , right
@@ -220,15 +222,28 @@
         ++   Copyδ-encode
         ++ ( $ ∷ ^ ∷ input-encode )
 
-utm-test1 : utmStates × ( List  utmΣ ) × ( List  utmΣ )
-utm-test1 = Turing.taccept U-TM  input+Copyδ
+short-input : List utmΣ
+short-input = $  ∷ ０  ∷ ０  ∷  ０ ∷  * ∷
+    ０  ∷ ０  ∷  ０ ∷  １  ∷ ０  ∷ １ ∷ １  ∷  * ∷
+    ０  ∷ ０  ∷  １ ∷  ０  ∷ １  ∷ １ ∷ １  ∷  * ∷
+    ０  ∷ １  ∷  B  ∷  １ ∷  ０  ∷ １ ∷ ０  ∷  * ∷
+    １  ∷ ０  ∷  ０ ∷  ０ ∷  １  ∷ １ ∷ １  ∷  $ ∷
+    ^   ∷ ０  ∷  ０ ∷  １  ∷ １ ∷ []  
 
-utm-test2 : ℕ  → utmStates × ( List  utmΣ ) × ( List  utmΣ )
-utm-test2 n  = loop n (Turing.tstart U-TM) input+Copyδ []
+utm-test1 : List  utmΣ → utmStates × ( List  utmΣ ) × ( List  utmΣ )
+utm-test1 inp = Turing.taccept U-TM  inp
+
+{-# TERMINATING #-}
+utm-test2 : ℕ  → List  utmΣ  → utmStates × ( List  utmΣ ) × ( List  utmΣ )
+utm-test2 n inp  = loop n (Turing.tstart U-TM) inp []
   where
         loop :  ℕ → utmStates → ( List  utmΣ ) → ( List  utmΣ ) → utmStates × ( List  utmΣ ) × ( List  utmΣ )
         loop zero q L R = ( q , L , R )
-        loop (suc n) q L R with  move {utmStates} {utmΣ} {０} {utmδ} q L R
-        ... | nq , nL , nR = loop n nq nL nR
+        loop (suc n) q L R with  move {utmStates} {utmΣ} {０} {utmδ} q L R | q
+        ... | nq , nL , nR | reads = loop n nq nL nR
+        ... | nq , nL , nR | _ = loop (suc n) nq nL nR
 
-t1 = utm-test2 10
+t1 = utm-test2 20 short-input 
+
+t : (n : ℕ)  → utmStates × ( List  utmΣ ) × ( List  utmΣ )
+t n = utm-test2 n short-input