spin tv-eval example: 87 of 210 windows do not pass its own validator #22

Summary

Running the shipped spin trace-validation example against its own windows, with its
own harness and its own pass convention, 87 of 210 windows do not pass. The cause looks
like a modelling mismatch rather than a bug in the tooling, and a second, related
mismatch sits between reference_spec/spin.tla and the window generator. Details and
reproduction below; I may well be misreading the intended semantics, in which case I'd
be glad to be corrected.

Checked at 4751133.

1. examples/spin/ai_spec_1 fails 87 of its own 210 windows

tla_eval/skills/tv-eval/examples/spin/ai_spec_1/ ships TV_AcquireLock.tla,
TV_AcquireLock.cfg, windows_AcquireLock.ndjson and run_tv.py, whose
returncode == 12 is the pass convention. Running all 210 windows:

123 pass
 87 other (exit 0)

The 87 are explained exactly by one guard. AcquireLock(t) in ai_spec_1/spin.tla
requires pc[t] = "trying":

AcquireLock(t) ==
  /\ pc[t] = "trying"
  /\ lockState = "unlocked"
  ...

Of the 210 AcquireSuccess windows in action_windows.jsonl, the actor's recorded
pc is acquiring in 123 and idle in 87 — the uncontended case, where a thread
takes a free lock without first spinning. ai_spec_1 reaches locked from idle in
two transitions, RequestBlocking then AcquireLock, and the trace records only the
second. Since each window is checked in isolation, there is no room for the
intervening transition, so every uncontended acquire reads as a failure.

For contrast, reference_spec/spin.tla has AcquireLockDirect (idle → locked in
one step) and accepts all 210.

If the intended reading is that a window may be satisfied by a sequence of spec
transitions rather than exactly one, then TV_AcquireLock.tla's Next (guarded by
step = 0, setting step' = 1) implements something stricter than that, and this
example is a case where the difference is visible.

2. reference_spec/spin.tla and generate_windows.py disagree about TryAcquireBlocking

generate_windows.py computes every post_state from an ACTION_EFFECTS table:

"TryAcquireBlocking": lambda state, actor: _set_pc(state, actor, "acquiring"),

This moves pc[actor] to acquiring unconditionally. reference_spec/spin.tla
guards the corresponding action on the lock being held:

\* Thread starts a blocking acquire attempt (lock is held, will spin)
TryAcquire(t) ==
    /\ pc[t] = "idle"
    /\ lockState = "locked"
    ...

So a blocking acquire that begins while the lock is free is a transition for the
generator and not for the reference spec. 104 of the 123 TryAcquireBlocking windows
are of that shape, and none of them is a transition of reference_spec/spin.tla —
under any number of intervening steps, since TryAcquire leaves lockState unchanged
and the recorded post-state has it unlocked.

Nothing shipped validates those windows: ai_spec_1/make_windows.py sets
TARGET_ACTION = "AcquireSuccess", and reference_spec/ ships no validator, so the
mismatch is not currently reachable through the example pipelines. ai_spec_1's
RequestBlocking has no lockState guard and agrees with the generator.

I could not work out which of the two is right about the system, because the raw traces
the windows are derived from (data/sys_traces/spin/, per generate_windows.py) are
not in the repository, and trace_loader.py documents that as intentional. The only
cross-check in the generator is a WARNING comparing computed lockState against the
trace's state field, which does not fail the run.

3. Minor: run_tv.py expects a lib/ directory that is not in the repo

PROJECT_ROOT = SPEC_DIR.resolve().parents[5]
TLA_JAR = str(PROJECT_ROOT / "lib" / "tla2tools.jar")
COMM_JAR = str(PROJECT_ROOT / "lib" / "CommunityModules-deps.jar")

There is no lib/ at that path in a fresh clone, so run_tv.py cannot run as shipped.
I substituted my own copies of both jars.

Reproduction

For section 1, one JVM per window with their flags, since run_tv.py cannot resolve
its jars:

cd tla_eval/skills/tv-eval/examples/spin/ai_spec_1
for i in $(seq 1 210); do
  WINDOW_INDEX=$i java -cp /path/to/tla2tools.jar:/path/to/CommunityModules-deps.jar \
    tlc2.TLC -dfid 2 -deadlock -nowarning -metadir /tmp/tv_spin_$i \
    -config TV_AcquireLock.cfg TV_AcquireLock.tla >/dev/null 2>&1
  echo "$i $?"
done | awk '{c[$2]++} END {for (k in c) print k, c[k]}'

For the window counts in sections 1 and 2, from the repository root:

python3 - <<'EOF'
import json, collections
ws = [json.loads(l) for l in open("tla_eval/skills/tv-eval/examples/spin/action_windows.jsonl") if l.strip()]
for action in ("AcquireSuccess", "TryAcquireBlocking"):
    c = collections.Counter(w["pre_state"]["pc"][w["actor"]] for w in ws if w["action"] == action)
    print(action, dict(c))
EOF

giving AcquireSuccess {'acquiring': 123, 'idle': 87} and
TryAcquireBlocking {'idle': 123}, of which 104 have lockState == "unlocked".

TLC used here is TLC2 Version 2026.10.01.024053 with the matching CommunityModules
release.

Context

These came out of comparing per-window transition validation against whole-trace
replay on the same windows, so the second conformance definition is mine and not
something this repo claims. Section 1 is entirely within your own pipeline, though,
and section 2 is a disagreement between two files that both ship here. Happy to send
the scripts if useful.