#!/usr/bin/env bash
# SPDX-FileCopyrightText: This work was generated by Claude Opus 4.8 in 2026.
#
# SPDX-License-Identifier: LicenseRef-No-Human-Authorship
#
# Torture-test the Turmac-to-Kondey compiler.
#
# Generates a batch of random *total, deterministic* Turmac machine
# descriptions and runs each one through `bisim-check-turmac`, which steps
# the Turmac simulator and the compiled Burro program in lockstep and
# compares their decoded configurations after every step (so a
# non-halting machine is fine -- it just runs to the step bound). Any
# per-step disagreement is a compiler bug; the offending description is
# saved so it can be replayed.
#
# Machines are generated total (every state/symbol pair gets exactly one
# rule) so they (a) satisfy the compiler's real precondition, (b) never
# make the simulator error on an undefined transition, and (c) can't hit
# the "gappy read set" rejection -- every mismatch is then a genuine
# discrepancy, not a generator artifact.
#
# Usage:
# ./torture-turmac.sh [MACHINES] [STEPS] [SEED]
#
# MACHINES how many random machines to try (default 100)
# STEPS step bound per machine (default 1000)
# SEED RNG seed, for reproducibility (default: time-based)
#
# On a slow machine, dial both down, e.g. `./torture-turmac.sh 20 200`.
# Failing descriptions are written to ./torture-failures/ and can be
# replayed with: ./bin/burro.exe bisim-check-turmac <file> <STEPS>
#
set -u
MACHINES="${1:-100}"
STEPS="${2:-1000}"
SEED="${3:-$(( ($$ ^ $(date +%s)) & 32767 ))}"
BURRO=./bin/burro.exe
FAILDIR=./torture-failures
if [ ! -x "$BURRO" ]; then
echo "error: $BURRO not found or not executable; run ./build.sh first" >&2
exit 2
fi
RANDOM=$SEED
WORKDIR="$(mktemp -d)"
trap 'rm -rf "$WORKDIR"' EXIT
echo "torture-turmac: $MACHINES machines x up to $STEPS steps, seed=$SEED"
# Pick a uniformly random element of the arguments.
pick() { eval "echo \${$(( (RANDOM % $#) + 1 ))}"; }
# Emit a random total, deterministic Turmac description on stdout.
# The start state is always S0 and the blank symbol is always `_`, as the
# simulator's initial configuration requires.
generate() {
local nstates=$(( (RANDOM % 4) + 2 )) # 2..5 states
local nsymbols=$(( (RANDOM % 3) + 2 )) # 2..4 symbols
local states=()
local i
for (( i = 0; i < nstates; i++ )); do states+=( "S$i" ); done
local sympool=(1 2 3)
local symbols=( _ )
for (( i = 0; i < nsymbols - 1; i++ )); do symbols+=( "${sympool[$i]}" ); done
echo "state,read,write,dir,newstate"
local st sym write dir newstate
for st in "${states[@]}"; do
for sym in "${symbols[@]}"; do
write=$(pick "${symbols[@]}")
dir=$(pick L R)
# Make the halt state uncommon so machines tend to run a while
# (and revisit cells -- the case where the once-latent carry bug
# surfaced), while still exercising the halting path sometimes.
if (( RANDOM % 15 == 0 )); then
newstate='@H'
else
newstate=$(pick "${states[@]}")
fi
echo "$st,$sym,$write,$dir,$newstate"
done
done
}
passes=0
fails=0
halted=0
running=0
for (( m = 1; m <= MACHINES; m++ )); do
tf="$WORKDIR/m$m.turmac"
generate > "$tf"
out="$("$BURRO" bisim-check-turmac "$tf" "$STEPS" 2>&1)"
status=$?
first="$(printf '%s\n' "$out" | head -n1)"
if [ "$status" -eq 0 ] && [ "$first" = "MATCH" ]; then
passes=$(( passes + 1 ))
case "$out" in
*halted*) halted=$(( halted + 1 )) ;;
*"still running"*) running=$(( running + 1 )) ;;
esac
else
fails=$(( fails + 1 ))
mkdir -p "$FAILDIR"
saved="$FAILDIR/fail-seed${SEED}-m${m}.turmac"
cp "$tf" "$saved"
echo
echo "MISMATCH on machine #$m (saved: $saved)"
printf '%s\n' "$out" | sed 's/^/ /'
echo " replay: $BURRO bisim-check-turmac $saved $STEPS"
fi
done
echo
echo "----------------------------------------------------------------"
echo "passed: $passes (halted: $halted, still running at bound: $running)"
echo "failed: $fails"
echo "seed: $SEED"
if [ "$fails" -ne 0 ]; then
echo "Failing descriptions saved under $FAILDIR/"
exit 1
fi
echo "All machines matched in lockstep. No compiler discrepancy found."