Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/utm.agda @ 407:c7ad8d2dc157
safe halt.agda
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Nov 2023 18:04:55 +0900 |
| parents | 6f3636fbc481 |
| children |
line wrap: on
line diff
--- a/automaton-in-agda/src/utm.agda Wed Nov 08 21:35:54 2023 +0900 +++ b/automaton-in-agda/src/utm.agda Thu Nov 09 18:04:55 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module utm where open import turing @@ -232,9 +234,8 @@ ^ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ [] utm-test1 : List utmΣ → utmStates × ( List utmΣ ) × ( List utmΣ ) -utm-test1 inp = Turing.taccept U-TM inp +utm-test1 inp = Turing.taccept U-TM 10 inp -{-# TERMINATING #-} utm-test2 : ℕ → List utmΣ → utmStates × ( List utmΣ ) × ( List utmΣ ) utm-test2 n inp = loop n (Turing.tstart U-TM) inp [] where @@ -242,7 +243,7 @@ loop zero q L R = ( q , L , R ) 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 + ... | nq , nL , nR | _ = loop n nq nL nR t1 = utm-test2 3 short-input