FA-66966 / Railway interlocking logic / Open access
Axle counter section supervision: reset acceptance · case 01
An operator reset of a miscounted or a disturbed section is ignored.
ROOT CAUSE
The reset is only accepted for a disturbed section, not for one stuck with a residual count.
VERIFIED REPAIR
Accept a reset when the section is disturbed or holds a non-zero count.
Unsuccessful approach: Accepting only non-zero counts refuses the reset of a disturbed section whose count was forced to zero.
Case contract
An axle-counter section counts axles in and out. Counting out below zero latches disturbed (count forced to 0). A reset is accepted only when the section is disturbed or the count is non-zero; it zeroes the count and enters preparatory state, which ends only when a sweep train has counted in and the count returns to zero on an out-count. query reports disturbed, prep, occupied (count>0) or clear, in that precedence.
Why this case matters
Interlocking logic decides whether trains may be given authority; a wrong decision at this point either grants unsafe movements or strands traffic.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(x):
count = 0
disturbed = False
prep = False
swept = False
out = []
for ev in x['events']:
if ev == 'in':
count += 1
if prep:
swept = True
elif ev == 'out':
count -= 1
if count < 0:
disturbed = True
count = 0
if prep and swept and count == 0:
prep = False
elif ev == 'reset':
if disturbed:
count = 0
disturbed = False
prep = True
swept = False
elif ev == 'query':
if disturbed:
out.append('disturbed')
elif prep:
out.append('prep')
elif count > 0:
out.append('occupied')
else:
out.append('clear')
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: reset of a miscounted section', {'events': ['in', 'in', 'out', 'reset', 'query', 'in', 'in', 'query', 'out', 'out', 'query']}, ['prep', 'prep', 'clear']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 9', {'events': ['in', 'query', 'query', 'reset', 'in', 'in', 'in', 'in', 'query', 'reset', 'in', 'query']}, ['occupied', 'occupied', 'prep', 'prep']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('boundary: under-count latches disturbance', {'events': ['out', 'query', 'in', 'query']}, ['disturbed', 'disturbed']), ('control 1', {'events': ['out', 'in', 'out', 'query', 'out', 'query', 'in', 'out', 'in', 'out', 'query', 'query', 'in', 'query', 'query']}, ['disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed']), ('control 4', {'events': ['in', 'out', 'query', 'query', 'query']}, ['clear', 'clear', 'clear']), ('control 7', {'events': ['query', 'out', 'in', 'query', 'out', 'query', 'reset', 'reset', 'in', 'reset', 'query', 'reset', 'query']}, ['clear', 'disturbed', 'disturbed', 'prep', 'prep'])], [('regression: under-count during preparation', {'events': ['in', 'reset', 'out', 'query']}, ['disturbed']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 62', {'events': ['in', 'in', 'in', 'reset', 'out', 'in', 'reset', 'query']}, ['prep']), ('control 29', {'events': ['out', 'in', 'in', 'out', 'out', 'in', 'reset', 'out', 'reset', 'in', 'query', 'in', 'query']}, ['prep', 'prep']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('control 12', {'events': ['query', 'out', 'reset', 'out', 'query']}, ['clear', 'disturbed']), ('control 15', {'events': ['out', 'out', 'in', 'reset', 'query', 'query', 'query']}, ['prep', 'prep', 'prep']), ('control 18', {'events': ['out', 'query', 'query', 'reset', 'in', 'query', 'query']}, ['disturbed', 'disturbed', 'prep', 'prep'])], [('regression: reset of a miscounted section', {'events': ['in', 'in', 'out', 'reset', 'query', 'in', 'in', 'query', 'out', 'out', 'query']}, ['prep', 'prep', 'clear']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 2', {'events': ['in', 'in', 'reset', 'reset', 'query', 'in', 'query']}, ['prep', 'prep']), ('control 79', {'events': ['reset', 'out', 'out', 'query', 'query', 'reset', 'query']}, ['disturbed', 'disturbed', 'prep']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('control 23', {'events': ['query', 'out', 'query', 'out', 'in', 'in', 'in', 'query', 'out', 'in', 'in', 'query']}, ['clear', 'disturbed', 'disturbed', 'disturbed']), ('control 26', {'events': ['reset', 'query', 'in', 'query']}, ['clear', 'occupied']), ('control 29', {'events': ['out', 'in', 'in', 'out', 'out', 'in', 'reset', 'out', 'reset', 'in', 'query', 'in', 'query']}, ['prep', 'prep'])], [('regression: under-count during preparation', {'events': ['in', 'reset', 'out', 'query']}, ['disturbed']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 57', {'events': ['in', 'query', 'in', 'out', 'reset', 'reset', 'in', 'query', 'out', 'query', 'query', 'in', 'in', 'query', 'query']}, ['occupied', 'prep', 'clear', 'clear', 'occupied', 'occupied']), ('control 18', {'events': ['out', 'query', 'query', 'reset', 'in', 'query', 'query']}, ['disturbed', 'disturbed', 'prep', 'prep']), ('boundary: normal passage', {'events': ['in', 'in', 'query', 'out', 'out', 'query']}, ['occupied', 'clear']), ('control 34', {'events': ['in', 'out', 'in', 'out', 'in', 'in', 'query']}, ['occupied']), ('control 37', {'events': ['reset', 'query', 'out', 'query', 'query', 'out', 'in', 'out', 'in', 'out', 'in', 'query']}, ['clear', 'disturbed', 'disturbed', 'disturbed']), ('control 40', {'events': ['in', 'in', 'query', 'out', 'query']}, ['occupied', 'occupied'])], [('regression: reset of a miscounted section', {'events': ['in', 'in', 'out', 'reset', 'query', 'in', 'in', 'query', 'out', 'out', 'query']}, ['prep', 'prep', 'clear']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('regression: under-count during preparation', {'events': ['in', 'reset', 'out', 'query']}, ['disturbed']), ('control 48', {'events': ['out', 'query', 'in', 'out', 'reset', 'in', 'query', 'query', 'query', 'query']}, ['disturbed', 'prep', 'prep', 'prep', 'prep']), ('boundary: reset refused on a clear section', {'events': ['reset', 'query', 'in', 'query']}, ['clear', 'occupied']), ('control 45', {'events': ['out', 'query', 'out', 'in', 'query', 'in', 'in', 'in', 'reset', 'in', 'query']}, ['disturbed', 'disturbed', 'prep']), ('control 51', {'events': ['reset', 'query', 'in', 'out', 'query', 'in', 'in', 'query', 'query', 'query', 'query']}, ['clear', 'clear', 'occupied', 'occupied', 'occupied', 'occupied']), ('sampled regression 54', {'events': ['query', 'query', 'in', 'in', 'out', 'in', 'query', 'out', 'query', 'reset', 'in', 'out', 'query', 'out', 'query']}, ['clear', 'clear', 'occupied', 'occupied', 'clear', 'disturbed'])]]
for label, args, expected in fixtures[N-1]:
check(label, solve(args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| regression: reset of a miscounted section | ['occupied', 'occupied', 'occupied'] | ['prep', 'prep', 'clear'] | Failed |
| boundary: reset of a disturbed section | ['prep', 'clear'] | ['prep', 'clear'] | Passed |
| sampled regression 9 | ['occupied', 'occupied', 'occupied', 'occupied'] | ['occupied', 'occupied', 'prep', 'prep'] | Failed |
| boundary: sweep train partly through | ['prep', 'clear'] | ['prep', 'clear'] | Passed |
| boundary: under-count latches disturbance | ['disturbed', 'disturbed'] | ['disturbed', 'disturbed'] | Passed |
| control 1 | ['disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed'] | ['disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed'] | Passed |
| control 4 | ['clear', 'clear', 'clear'] | ['clear', 'clear', 'clear'] | Passed |
| control 7 | ['clear', 'disturbed', 'disturbed', 'prep', 'prep'] | ['clear', 'disturbed', 'disturbed', 'prep', 'prep'] | Passed |
SHA-256 / cac4d623f03b4f343790dad9863feccd57634995d13abe011bc90ee838febeeb
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(x):
count = 0
disturbed = False
prep = False
swept = False
out = []
for ev in x['events']:
if ev == 'in':
count += 1
if prep:
swept = True
elif ev == 'out':
count -= 1
if count < 0:
disturbed = True
count = 0
if prep and swept and count == 0:
prep = False
elif ev == 'reset':
if count != 0:
count = 0
disturbed = False
prep = True
swept = False
elif ev == 'query':
if disturbed:
out.append('disturbed')
elif prep:
out.append('prep')
elif count > 0:
out.append('occupied')
else:
out.append('clear')
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: reset of a miscounted section', {'events': ['in', 'in', 'out', 'reset', 'query', 'in', 'in', 'query', 'out', 'out', 'query']}, ['prep', 'prep', 'clear']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 9', {'events': ['in', 'query', 'query', 'reset', 'in', 'in', 'in', 'in', 'query', 'reset', 'in', 'query']}, ['occupied', 'occupied', 'prep', 'prep']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('boundary: under-count latches disturbance', {'events': ['out', 'query', 'in', 'query']}, ['disturbed', 'disturbed']), ('control 1', {'events': ['out', 'in', 'out', 'query', 'out', 'query', 'in', 'out', 'in', 'out', 'query', 'query', 'in', 'query', 'query']}, ['disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed']), ('control 4', {'events': ['in', 'out', 'query', 'query', 'query']}, ['clear', 'clear', 'clear']), ('control 7', {'events': ['query', 'out', 'in', 'query', 'out', 'query', 'reset', 'reset', 'in', 'reset', 'query', 'reset', 'query']}, ['clear', 'disturbed', 'disturbed', 'prep', 'prep'])], [('regression: under-count during preparation', {'events': ['in', 'reset', 'out', 'query']}, ['disturbed']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 62', {'events': ['in', 'in', 'in', 'reset', 'out', 'in', 'reset', 'query']}, ['prep']), ('control 29', {'events': ['out', 'in', 'in', 'out', 'out', 'in', 'reset', 'out', 'reset', 'in', 'query', 'in', 'query']}, ['prep', 'prep']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('control 12', {'events': ['query', 'out', 'reset', 'out', 'query']}, ['clear', 'disturbed']), ('control 15', {'events': ['out', 'out', 'in', 'reset', 'query', 'query', 'query']}, ['prep', 'prep', 'prep']), ('control 18', {'events': ['out', 'query', 'query', 'reset', 'in', 'query', 'query']}, ['disturbed', 'disturbed', 'prep', 'prep'])], [('regression: reset of a miscounted section', {'events': ['in', 'in', 'out', 'reset', 'query', 'in', 'in', 'query', 'out', 'out', 'query']}, ['prep', 'prep', 'clear']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 2', {'events': ['in', 'in', 'reset', 'reset', 'query', 'in', 'query']}, ['prep', 'prep']), ('control 79', {'events': ['reset', 'out', 'out', 'query', 'query', 'reset', 'query']}, ['disturbed', 'disturbed', 'prep']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('control 23', {'events': ['query', 'out', 'query', 'out', 'in', 'in', 'in', 'query', 'out', 'in', 'in', 'query']}, ['clear', 'disturbed', 'disturbed', 'disturbed']), ('control 26', {'events': ['reset', 'query', 'in', 'query']}, ['clear', 'occupied']), ('control 29', {'events': ['out', 'in', 'in', 'out', 'out', 'in', 'reset', 'out', 'reset', 'in', 'query', 'in', 'query']}, ['prep', 'prep'])], [('regression: under-count during preparation', {'events': ['in', 'reset', 'out', 'query']}, ['disturbed']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 57', {'events': ['in', 'query', 'in', 'out', 'reset', 'reset', 'in', 'query', 'out', 'query', 'query', 'in', 'in', 'query', 'query']}, ['occupied', 'prep', 'clear', 'clear', 'occupied', 'occupied']), ('control 18', {'events': ['out', 'query', 'query', 'reset', 'in', 'query', 'query']}, ['disturbed', 'disturbed', 'prep', 'prep']), ('boundary: normal passage', {'events': ['in', 'in', 'query', 'out', 'out', 'query']}, ['occupied', 'clear']), ('control 34', {'events': ['in', 'out', 'in', 'out', 'in', 'in', 'query']}, ['occupied']), ('control 37', {'events': ['reset', 'query', 'out', 'query', 'query', 'out', 'in', 'out', 'in', 'out', 'in', 'query']}, ['clear', 'disturbed', 'disturbed', 'disturbed']), ('control 40', {'events': ['in', 'in', 'query', 'out', 'query']}, ['occupied', 'occupied'])], [('regression: reset of a miscounted section', {'events': ['in', 'in', 'out', 'reset', 'query', 'in', 'in', 'query', 'out', 'out', 'query']}, ['prep', 'prep', 'clear']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('regression: under-count during preparation', {'events': ['in', 'reset', 'out', 'query']}, ['disturbed']), ('control 48', {'events': ['out', 'query', 'in', 'out', 'reset', 'in', 'query', 'query', 'query', 'query']}, ['disturbed', 'prep', 'prep', 'prep', 'prep']), ('boundary: reset refused on a clear section', {'events': ['reset', 'query', 'in', 'query']}, ['clear', 'occupied']), ('control 45', {'events': ['out', 'query', 'out', 'in', 'query', 'in', 'in', 'in', 'reset', 'in', 'query']}, ['disturbed', 'disturbed', 'prep']), ('control 51', {'events': ['reset', 'query', 'in', 'out', 'query', 'in', 'in', 'query', 'query', 'query', 'query']}, ['clear', 'clear', 'occupied', 'occupied', 'occupied', 'occupied']), ('sampled regression 54', {'events': ['query', 'query', 'in', 'in', 'out', 'in', 'query', 'out', 'query', 'reset', 'in', 'out', 'query', 'out', 'query']}, ['clear', 'clear', 'occupied', 'occupied', 'clear', 'disturbed'])]]
for label, args, expected in fixtures[N-1]:
check(label, solve(args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| regression: reset of a miscounted section | ['prep', 'prep', 'clear'] | ['prep', 'prep', 'clear'] | Passed |
| boundary: reset of a disturbed section | ['disturbed', 'disturbed'] | ['prep', 'clear'] | Failed |
| sampled regression 9 | ['occupied', 'occupied', 'prep', 'prep'] | ['occupied', 'occupied', 'prep', 'prep'] | Passed |
| boundary: sweep train partly through | ['disturbed', 'disturbed'] | ['prep', 'clear'] | Failed |
| boundary: under-count latches disturbance | ['disturbed', 'disturbed'] | ['disturbed', 'disturbed'] | Passed |
| control 1 | ['disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed'] | ['disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed'] | Passed |
| control 4 | ['clear', 'clear', 'clear'] | ['clear', 'clear', 'clear'] | Passed |
| control 7 | ['clear', 'disturbed', 'disturbed', 'prep', 'prep'] | ['clear', 'disturbed', 'disturbed', 'prep', 'prep'] | Passed |
SHA-256 / 00cbfa4cc619e366ab800862bda37cf404e8e9ee365ee70f66fca4a56c10e223
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(x):
count = 0
disturbed = False
prep = False
swept = False
out = []
for ev in x['events']:
if ev == 'in':
count += 1
if prep:
swept = True
elif ev == 'out':
count -= 1
if count < 0:
disturbed = True
count = 0
if prep and swept and count == 0:
prep = False
elif ev == 'reset':
if disturbed or count != 0:
count = 0
disturbed = False
prep = True
swept = False
elif ev == 'query':
if disturbed:
out.append('disturbed')
elif prep:
out.append('prep')
elif count > 0:
out.append('occupied')
else:
out.append('clear')
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: reset of a miscounted section', {'events': ['in', 'in', 'out', 'reset', 'query', 'in', 'in', 'query', 'out', 'out', 'query']}, ['prep', 'prep', 'clear']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 9', {'events': ['in', 'query', 'query', 'reset', 'in', 'in', 'in', 'in', 'query', 'reset', 'in', 'query']}, ['occupied', 'occupied', 'prep', 'prep']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('boundary: under-count latches disturbance', {'events': ['out', 'query', 'in', 'query']}, ['disturbed', 'disturbed']), ('control 1', {'events': ['out', 'in', 'out', 'query', 'out', 'query', 'in', 'out', 'in', 'out', 'query', 'query', 'in', 'query', 'query']}, ['disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed']), ('control 4', {'events': ['in', 'out', 'query', 'query', 'query']}, ['clear', 'clear', 'clear']), ('control 7', {'events': ['query', 'out', 'in', 'query', 'out', 'query', 'reset', 'reset', 'in', 'reset', 'query', 'reset', 'query']}, ['clear', 'disturbed', 'disturbed', 'prep', 'prep'])], [('regression: under-count during preparation', {'events': ['in', 'reset', 'out', 'query']}, ['disturbed']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 62', {'events': ['in', 'in', 'in', 'reset', 'out', 'in', 'reset', 'query']}, ['prep']), ('control 29', {'events': ['out', 'in', 'in', 'out', 'out', 'in', 'reset', 'out', 'reset', 'in', 'query', 'in', 'query']}, ['prep', 'prep']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('control 12', {'events': ['query', 'out', 'reset', 'out', 'query']}, ['clear', 'disturbed']), ('control 15', {'events': ['out', 'out', 'in', 'reset', 'query', 'query', 'query']}, ['prep', 'prep', 'prep']), ('control 18', {'events': ['out', 'query', 'query', 'reset', 'in', 'query', 'query']}, ['disturbed', 'disturbed', 'prep', 'prep'])], [('regression: reset of a miscounted section', {'events': ['in', 'in', 'out', 'reset', 'query', 'in', 'in', 'query', 'out', 'out', 'query']}, ['prep', 'prep', 'clear']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 2', {'events': ['in', 'in', 'reset', 'reset', 'query', 'in', 'query']}, ['prep', 'prep']), ('control 79', {'events': ['reset', 'out', 'out', 'query', 'query', 'reset', 'query']}, ['disturbed', 'disturbed', 'prep']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('control 23', {'events': ['query', 'out', 'query', 'out', 'in', 'in', 'in', 'query', 'out', 'in', 'in', 'query']}, ['clear', 'disturbed', 'disturbed', 'disturbed']), ('control 26', {'events': ['reset', 'query', 'in', 'query']}, ['clear', 'occupied']), ('control 29', {'events': ['out', 'in', 'in', 'out', 'out', 'in', 'reset', 'out', 'reset', 'in', 'query', 'in', 'query']}, ['prep', 'prep'])], [('regression: under-count during preparation', {'events': ['in', 'reset', 'out', 'query']}, ['disturbed']), ('boundary: sweep train partly through', {'events': ['out', 'reset', 'in', 'in', 'out', 'query', 'out', 'query']}, ['prep', 'clear']), ('sampled regression 57', {'events': ['in', 'query', 'in', 'out', 'reset', 'reset', 'in', 'query', 'out', 'query', 'query', 'in', 'in', 'query', 'query']}, ['occupied', 'prep', 'clear', 'clear', 'occupied', 'occupied']), ('control 18', {'events': ['out', 'query', 'query', 'reset', 'in', 'query', 'query']}, ['disturbed', 'disturbed', 'prep', 'prep']), ('boundary: normal passage', {'events': ['in', 'in', 'query', 'out', 'out', 'query']}, ['occupied', 'clear']), ('control 34', {'events': ['in', 'out', 'in', 'out', 'in', 'in', 'query']}, ['occupied']), ('control 37', {'events': ['reset', 'query', 'out', 'query', 'query', 'out', 'in', 'out', 'in', 'out', 'in', 'query']}, ['clear', 'disturbed', 'disturbed', 'disturbed']), ('control 40', {'events': ['in', 'in', 'query', 'out', 'query']}, ['occupied', 'occupied'])], [('regression: reset of a miscounted section', {'events': ['in', 'in', 'out', 'reset', 'query', 'in', 'in', 'query', 'out', 'out', 'query']}, ['prep', 'prep', 'clear']), ('boundary: reset of a disturbed section', {'events': ['out', 'reset', 'query', 'in', 'out', 'query']}, ['prep', 'clear']), ('regression: under-count during preparation', {'events': ['in', 'reset', 'out', 'query']}, ['disturbed']), ('control 48', {'events': ['out', 'query', 'in', 'out', 'reset', 'in', 'query', 'query', 'query', 'query']}, ['disturbed', 'prep', 'prep', 'prep', 'prep']), ('boundary: reset refused on a clear section', {'events': ['reset', 'query', 'in', 'query']}, ['clear', 'occupied']), ('control 45', {'events': ['out', 'query', 'out', 'in', 'query', 'in', 'in', 'in', 'reset', 'in', 'query']}, ['disturbed', 'disturbed', 'prep']), ('control 51', {'events': ['reset', 'query', 'in', 'out', 'query', 'in', 'in', 'query', 'query', 'query', 'query']}, ['clear', 'clear', 'occupied', 'occupied', 'occupied', 'occupied']), ('sampled regression 54', {'events': ['query', 'query', 'in', 'in', 'out', 'in', 'query', 'out', 'query', 'reset', 'in', 'out', 'query', 'out', 'query']}, ['clear', 'clear', 'occupied', 'occupied', 'clear', 'disturbed'])]]
for label, args, expected in fixtures[N-1]:
check(label, solve(args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| regression: reset of a miscounted section | ['prep', 'prep', 'clear'] | ['prep', 'prep', 'clear'] | Passed |
| boundary: reset of a disturbed section | ['prep', 'clear'] | ['prep', 'clear'] | Passed |
| sampled regression 9 | ['occupied', 'occupied', 'prep', 'prep'] | ['occupied', 'occupied', 'prep', 'prep'] | Passed |
| boundary: sweep train partly through | ['prep', 'clear'] | ['prep', 'clear'] | Passed |
| boundary: under-count latches disturbance | ['disturbed', 'disturbed'] | ['disturbed', 'disturbed'] | Passed |
| control 1 | ['disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed'] | ['disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed', 'disturbed'] | Passed |
| control 4 | ['clear', 'clear', 'clear'] | ['clear', 'clear', 'clear'] | Passed |
| control 7 | ['clear', 'disturbed', 'disturbed', 'prep', 'prep'] | ['clear', 'disturbed', 'disturbed', 'prep', 'prep'] | Passed |
SHA-256 / 4bc024d5121a4aacdb5ad690a6cab58fe5845ce3785b31df4547dee184fd0375
Verification & scope
Stipulated toy interlocking contract for a bounded teaching model; it makes no claim of conformance to any railway signalling standard and omits real safety cases. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.
Observations recorded using Python 3.12.14 at 2026-09-29T14:47:48.559592+00:00.
Case digest / c30452de00fd84bb3335f3eea896272408c5ca06ea0b1f9e170ca917c63b9030