diff --git a/test/lin_rec.py b/test/lin_rec.py index 12e1208b..eeafec6c 100644 --- a/test/lin_rec.py +++ b/test/lin_rec.py @@ -55,3 +55,103 @@ def run( self.cycles = cycle return self + + +class LooseLinRecMachine(LinRecMachine): + # pylint: disable = while-used, too-many-locals, line-too-long + def run(self, sim_lim: int) -> Self: # no-cover + self.blanks = {} + + comp = self.comp + + state = 1 + + step = 1 + + self.tape = tape = HeadTape.init_stepped() + + cycle = 1 + + while cycle < sim_lim: + steps_reset = 2 * step + + leftmost = rightmost = init_pos = tape.head + + init_state = state + + init_tape = tape.to_ptr() + + while step < steps_reset and cycle < sim_lim: + if (instr := comp[state, tape.scan]) is None: + self.undfnd = step, (state, tape.scan) + break + + color, shift, next_state = instr + + if (same := state == next_state) and tape.at_edge(shift): + self.spnout = step + break + + stepped = tape.step(shift, color, same) + + step += stepped + + cycle += 1 + + if (state := next_state) == -1: + self.halted = step + break + + if not color and tape.blank: + if state in self.blanks: + self.infrul = step + break + + self.blanks[state] = step + + if state == 0: + self.infrul = step + break + + if (curr := tape.head) < leftmost: + leftmost = curr + elif rightmost < curr: + rightmost = curr + + if state != init_state: + continue + + if tape.scan != init_tape.scan: + continue + + ptr = tape.to_ptr() + + if 0 < (diff := curr - init_pos): + slice1 = init_tape.get_ltr(leftmost) + slice2 = ptr.get_ltr(leftmost + diff) + + elif diff < 0: + slice1 = init_tape.get_rtl(rightmost) + slice2 = ptr.get_rtl(rightmost + diff) + + else: + slice1 = init_tape.get_cnt(leftmost, rightmost) + slice2 = ptr.get_cnt(leftmost, rightmost) + + if slice1 == slice2: + self.infrul = step + break + + else: + continue + + self.xlimit = None + + break + + else: + self.xlimit = stepped + + self.cycles = cycle + + return self diff --git a/test/test_lin_rado.py b/test/test_lin_rado.py index 91853582..1d4a6e52 100644 --- a/test/test_lin_rado.py +++ b/test/test_lin_rado.py @@ -11,7 +11,7 @@ from tm.show import show_state from tm.lin_rec import ( StrictLinRecMachine, - LooseLinRecMachine, + quick_term_or_rec, ) if TYPE_CHECKING: @@ -66,9 +66,7 @@ def run_lin_rado( bool(halt), rejects) if - LooseLinRecMachine(prog).run( - sim_lim = loose, - ).xlimit is not None + not quick_term_or_rec(prog, loose) } def test_22(self): diff --git a/test/test_tree.py b/test/test_tree.py index 5f479157..8af5fb2c 100644 --- a/test/test_tree.py +++ b/test/test_tree.py @@ -5,9 +5,10 @@ from typing import TYPE_CHECKING from test.utils import read_progs +from test.lin_rec import LooseLinRecMachine from tm.machine import Machine -from tm.lin_rec import LooseLinRecMachine +from tm.lin_rec import quick_term_or_rec from tm.reason import BackwardReasoner, cant_halt, cant_spin_out from tm.tree import run_tree_gen @@ -281,12 +282,10 @@ def capture(prog: str) -> None: if 'D' not in prog: return - machines = run_variations( - prog, 1000, - lin_rec = 50, - ) + if quick_term_or_rec(prog, 50): + return - for machine in machines: + for machine in run_variations(prog, 1000): if machine.xlimit is None: self.add_result(prog, machine) return @@ -332,9 +331,11 @@ def capture(prog: str) -> None: if '3' not in prog: return + if quick_term_or_rec(prog, 100): + return + machines = run_variations( prog, 3_000, - lin_rec = 100, block_steps = 6_000, ) @@ -369,7 +370,7 @@ def capture(prog: str) -> None: if cant_spin_out(prog): return - if LooseLinRecMachine(prog).run(1_000).xlimit is None: + if quick_term_or_rec(prog, 1_000): return machine = Machine( diff --git a/test/test_turing.py b/test/test_turing.py index 069f5bf1..74d0bb38 100644 --- a/test/test_turing.py +++ b/test/test_turing.py @@ -8,7 +8,7 @@ # pylint: disable-next = wildcard-import, unused-wildcard-import from test.prog_data import * -from test.lin_rec import LinRecSampler +from test.lin_rec import LinRecSampler, LooseLinRecMachine from test.test_num import assert_num_counts, clear_caches from tm.reason import ( @@ -24,7 +24,7 @@ QuickMachine, Machine, ) -from tm.lin_rec import StrictLinRecMachine, LooseLinRecMachine +from tm.lin_rec import StrictLinRecMachine, quick_term_or_rec from tools.instr_seq import instr_seq @@ -426,6 +426,9 @@ def _test_recur( 100_000 ).infrul) + self.assertTrue( + quick_term_or_rec(prog, 100_000)) + def _test_prover( # type: ignore[misc] self, prog_data: Mapping[str, Any], diff --git a/tm/lin_rec.py b/tm/lin_rec.py index 7aaae0c9..8afed7a7 100644 --- a/tm/lin_rec.py +++ b/tm/lin_rec.py @@ -390,101 +390,70 @@ def check_rec(self, step: int, slot: Slot) -> RecRes | None: return result -class LooseLinRecMachine(LinRecMachine): - # pylint: disable = while-used, too-many-locals, line-too-long - def run(self, sim_lim: int) -> Self: # no-cover - self.blanks = {} - - comp = self.comp +def quick_term_or_rec(prog: str, sim_lim: int) -> bool: # no-cover + # pylint: disable = while-used, too-many-locals - state = 1 + comp = tcompile(prog) - step = 1 + state = 1 - self.tape = tape = HeadTape.init_stepped() + tape = HeadTape.init_stepped() - cycle = 1 + step, cycle = 1, 1 - while cycle < sim_lim: - steps_reset = 2 * step + while cycle < sim_lim: + steps_reset = 2 * step - leftmost = rightmost = init_pos = tape.head + leftmost = rightmost = init_pos = tape.head - init_state = state + init_state = state - init_tape = tape.to_ptr() + init_tape = tape.to_ptr() - while step < steps_reset and cycle < sim_lim: - if (instr := comp[state, tape.scan]) is None: - self.undfnd = step, (state, tape.scan) - break - - color, shift, next_state = instr + while step < steps_reset and cycle < sim_lim: + if (instr := comp[state, tape.scan]) is None: + return True - if (same := state == next_state) and tape.at_edge(shift): - self.spnout = step - break - - stepped = tape.step(shift, color, same) - - step += stepped - - cycle += 1 - - if (state := next_state) == -1: - self.halted = step - break + color, shift, next_state = instr - if not color and tape.blank: - if state in self.blanks: - self.infrul = step - break + if (same := state == next_state) and tape.at_edge(shift): + return True - self.blanks[state] = step + stepped = tape.step(shift, color, same) - if state == 0: - self.infrul = step - break + step += stepped - if (curr := tape.head) < leftmost: - leftmost = curr - elif rightmost < curr: - rightmost = curr + cycle += 1 - if state != init_state: - continue + if (state := next_state) == -1: + return True - if tape.scan != init_tape.scan: - continue + if (curr := tape.head) < leftmost: + leftmost = curr + elif rightmost < curr: + rightmost = curr - ptr = tape.to_ptr() + if state != init_state: + continue - if 0 < (diff := curr - init_pos): - slice1 = init_tape.get_ltr(leftmost) - slice2 = ptr.get_ltr(leftmost + diff) + if tape.scan != init_tape.scan: + continue - elif diff < 0: - slice1 = init_tape.get_rtl(rightmost) - slice2 = ptr.get_rtl(rightmost + diff) + ptr = tape.to_ptr() - else: - slice1 = init_tape.get_cnt(leftmost, rightmost) - slice2 = ptr.get_cnt(leftmost, rightmost) + if 0 < (diff := curr - init_pos): + slice1 = init_tape.get_ltr(leftmost) + slice2 = ptr.get_ltr(leftmost + diff) - if slice1 == slice2: - self.infrul = step - break + elif diff < 0: + slice1 = init_tape.get_rtl(rightmost) + slice2 = ptr.get_rtl(rightmost + diff) else: - continue - - self.xlimit = None + slice1 = init_tape.get_cnt(leftmost, rightmost) + slice2 = ptr.get_cnt(leftmost, rightmost) - break + if slice1 == slice2: + return True - else: - self.xlimit = stepped - - self.cycles = cycle - - return self + return False diff --git a/tree_gen.py b/tree_gen.py index 0da39001..58f9b5df 100644 --- a/tree_gen.py +++ b/tree_gen.py @@ -4,7 +4,7 @@ from tm.reason import cant_halt, cant_spin_out from tm.machine import Machine -from tm.lin_rec import LooseLinRecMachine +from tm.lin_rec import quick_term_or_rec from tm.tree import run_tree_gen @@ -16,7 +16,7 @@ def run_variations( lin_rec: int = 1_000, block_steps: int = 1_000, ) -> Machine | None: - if LooseLinRecMachine(prog).run(lin_rec).xlimit is None: + if quick_term_or_rec(prog, lin_rec): return None machine = Machine(