# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1584182547 -32400
# Node ID 4c3fbfde1bc27954c415423192c02a4d7fe9029c
# Parent  3be1afb87f8235d3cd8b2fd6f1d5b17a297addbb
utm tester

diff -r 3be1afb87f82 -r 4c3fbfde1bc2 agda/utm.agda
--- 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