FA-67031 / Railway interlocking logic / Open access
Overlap timed release: berth clear cancellation · case 01
The overlap is released after the train has already left the berth.
ROOT CAUSE
A berth clear never cancels the running timer.
VERIFIED REPAIR
Cancel the timer on berth clear unless the overlap is already released.
Unsuccessful approach: Cancelling unconditionally re-locks an overlap that was already released.
Case contract
The overlap beyond a signal is locked. The release timer starts at the first berth occupation; the overlap is released when an event time reaches start + timer_s while the train has not overrun into the overlap. A berth clear before release cancels the timer (a later occupation restarts it); after release it has no effect. Entering the overlap before release marks an overrun and blocks release. query appends locked or released.
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):
T = x['timer_s']
start = None
overran = False
released = False
out = []
for t, ev in x['events']:
if start is not None and not released and not overran and t - start >= T:
released = True
if ev == 'berth_occ':
if start is None:
start = t
elif ev == 'berth_clr':
pass
elif ev == 'overlap_occ':
if not released:
overran = True
elif ev == 'query':
out.append('released' if released else 'locked')
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 51', {'timer_s': 90, 'events': [[90, 'berth_occ'], [150, 'berth_clr'], [195, 'query'], [255, 'berth_occ'], [315, 'query'], [320, 'query'], [320, 'overlap_occ'], [440, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 18', {'timer_s': 90, 'events': [[0, 'query'], [0, 'query'], [30, 'berth_occ'], [120, 'overlap_occ'], [210, 'berth_clr'], [215, 'query'], [245, 'berth_occ'], [365, 'query']]}, ['locked', 'locked', 'released', 'released']), ('boundary: expiry exactly on time', {'timer_s': 60, 'events': [[10, 'berth_occ'], [70, 'query']]}, ['released']), ('control 1', {'timer_s': 45, 'events': [[5, 'overlap_occ'], [35, 'query'], [65, 'berth_clr'], [125, 'query'], [170, 'query'], [170, 'berth_clr'], [230, 'berth_occ'], [350, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 4', {'timer_s': 90, 'events': [[60, 'berth_clr'], [150, 'berth_occ'], [155, 'berth_occ'], [155, 'query']]}, ['locked']), ('control 7', {'timer_s': 45, 'events': [[5, 'query'], [65, 'overlap_occ'], [110, 'overlap_occ'], [170, 'query']]}, ['locked', 'locked'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('control 59', {'timer_s': 45, 'events': [[30, 'query'], [120, 'query'], [120, 'berth_occ'], [210, 'query'], [215, 'berth_clr'], [215, 'berth_clr'], [215, 'berth_clr'], [275, 'query']]}, ['locked', 'locked', 'released', 'released']), ('boundary: train stops at time zero', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_occ'], [60, 'query']]}, ['released']), ('boundary: overrun into the overlap', {'timer_s': 60, 'events': [[0, 'berth_occ'], [20, 'overlap_occ'], [120, 'query']]}, ['locked']), ('control 12', {'timer_s': 120, 'events': [[60, 'berth_occ'], [65, 'query'], [70, 'query'], [70, 'query'], [75, 'berth_occ'], [80, 'berth_occ'], [125, 'berth_clr'], [125, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 15', {'timer_s': 120, 'events': [[60, 'berth_clr'], [105, 'berth_clr'], [110, 'berth_clr'], [115, 'berth_clr'], [175, 'query'], [175, 'berth_clr'], [235, 'query'], [265, 'overlap_occ'], [270, 'berth_clr'], [390, 'query']]}, ['locked', 'locked', 'locked']), ('control 18', {'timer_s': 90, 'events': [[0, 'query'], [0, 'query'], [30, 'berth_occ'], [120, 'overlap_occ'], [210, 'berth_clr'], [215, 'query'], [245, 'berth_occ'], [365, 'query']]}, ['locked', 'locked', 'released', 'released'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 9', {'timer_s': 60, 'events': [[5, 'berth_occ'], [5, 'query'], [35, 'berth_clr'], [155, 'query']]}, ['locked', 'locked']), ('control 78', {'timer_s': 90, 'events': [[0, 'query'], [90, 'berth_occ'], [120, 'berth_occ'], [120, 'query'], [210, 'berth_clr'], [210, 'query']]}, ['locked', 'locked', 'released']), ('boundary: overrun into the overlap', {'timer_s': 60, 'events': [[0, 'berth_occ'], [20, 'overlap_occ'], [120, 'query']]}, ['locked']), ('control 23', {'timer_s': 45, 'events': [[0, 'query'], [5, 'berth_occ'], [95, 'berth_occ'], [185, 'berth_occ'], [245, 'query']]}, ['locked', 'released']), ('control 26', {'timer_s': 60, 'events': [[30, 'query'], [60, 'query'], [150, 'overlap_occ'], [150, 'query']]}, ['locked', 'locked', 'locked']), ('control 29', {'timer_s': 90, 'events': [[90, 'overlap_occ'], [95, 'query'], [95, 'berth_occ'], [185, 'query'], [230, 'query'], [260, 'query'], [350, 'berth_occ'], [410, 'query']]}, ['locked', 'locked', 'locked', 'locked', 'locked'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 75', {'timer_s': 90, 'events': [[0, 'berth_occ'], [0, 'query'], [60, 'berth_clr'], [120, 'query'], [180, 'overlap_occ'], [225, 'berth_occ'], [270, 'query'], [275, 'berth_occ'], [320, 'overlap_occ'], [380, 'berth_occ'], [380, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 33', {'timer_s': 60, 'events': [[60, 'berth_occ'], [60, 'query'], [120, 'query'], [150, 'berth_occ'], [240, 'berth_clr'], [360, 'query']]}, ['locked', 'released', 'released']), ('boundary: ninety second timer at one minute', {'timer_s': 90, 'events': [[0, 'berth_occ'], [60, 'query'], [89, 'query'], [90, 'query']]}, ['locked', 'locked', 'released']), ('control 34', {'timer_s': 60, 'events': [[5, 'query'], [35, 'query'], [80, 'berth_occ'], [170, 'berth_occ'], [260, 'berth_occ'], [320, 'berth_occ'], [350, 'overlap_occ'], [395, 'overlap_occ'], [440, 'query'], [500, 'query'], [560, 'query']]}, ['locked', 'locked', 'released', 'released', 'released']), ('control 37', {'timer_s': 120, 'events': [[30, 'query'], [60, 'overlap_occ'], [120, 'berth_occ'], [180, 'overlap_occ'], [185, 'overlap_occ'], [185, 'overlap_occ'], [245, 'query'], [275, 'query'], [280, 'overlap_occ'], [280, 'berth_occ'], [280, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 40', {'timer_s': 90, 'events': [[60, 'overlap_occ'], [90, 'query'], [135, 'berth_occ'], [195, 'overlap_occ'], [225, 'berth_occ'], [230, 'berth_clr'], [230, 'query']]}, ['locked', 'locked'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 8', {'timer_s': 120, 'events': [[30, 'berth_occ'], [120, 'berth_clr'], [165, 'berth_clr'], [170, 'berth_occ'], [215, 'berth_clr'], [215, 'overlap_occ'], [305, 'query'], [305, 'berth_occ'], [395, 'berth_occ'], [440, 'berth_occ'], [560, 'query']]}, ['locked', 'locked']), ('control 66', {'timer_s': 90, 'events': [[5, 'query'], [65, 'berth_occ'], [155, 'overlap_occ'], [160, 'overlap_occ'], [160, 'berth_occ'], [165, 'berth_occ'], [210, 'berth_occ'], [210, 'berth_clr'], [215, 'overlap_occ'], [275, 'overlap_occ'], [275, 'query']]}, ['locked', 'released']), ('boundary: expiry exactly on time', {'timer_s': 60, 'events': [[10, 'berth_occ'], [70, 'query']]}, ['released']), ('control 45', {'timer_s': 60, 'events': [[60, 'query'], [120, 'query'], [150, 'overlap_occ'], [155, 'berth_occ'], [245, 'overlap_occ'], [290, 'berth_occ'], [380, 'berth_clr'], [470, 'overlap_occ'], [470, 'query'], [475, 'berth_occ'], [595, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 48', {'timer_s': 45, 'events': [[60, 'overlap_occ'], [150, 'berth_occ'], [180, 'overlap_occ'], [180, 'berth_occ'], [270, 'berth_clr'], [275, 'berth_clr'], [275, 'overlap_occ'], [275, 'query']]}, ['locked']), ('sampled regression 51', {'timer_s': 90, 'events': [[90, 'berth_occ'], [150, 'berth_clr'], [195, 'query'], [255, 'berth_occ'], [315, 'query'], [320, 'query'], [320, 'overlap_occ'], [440, 'query']]}, ['locked', 'locked', 'locked', 'locked'])]]
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: train leaves before expiry | ['released'] | ['locked'] | Failed |
| boundary: berth clears after release | ['released', 'released'] | ['released', 'released'] | Passed |
| sampled regression 51 | ['released', 'released', 'released', 'released'] | ['locked', 'locked', 'locked', 'locked'] | Failed |
| control 18 | ['locked', 'locked', 'released', 'released'] | ['locked', 'locked', 'released', 'released'] | Passed |
| boundary: expiry exactly on time | ['released'] | ['released'] | Passed |
| control 1 | ['locked', 'locked', 'locked', 'locked'] | ['locked', 'locked', 'locked', 'locked'] | Passed |
| control 4 | ['locked'] | ['locked'] | Passed |
| control 7 | ['locked', 'locked'] | ['locked', 'locked'] | Passed |
SHA-256 / 525d109cd0ba511b5317ac420cf1cbc4e515f0ed3442b83a95bc0a4ea6ebb089
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(x):
T = x['timer_s']
start = None
overran = False
released = False
out = []
for t, ev in x['events']:
if start is not None and not released and not overran and t - start >= T:
released = True
if ev == 'berth_occ':
if start is None:
start = t
elif ev == 'berth_clr':
start = None
released = False
elif ev == 'overlap_occ':
if not released:
overran = True
elif ev == 'query':
out.append('released' if released else 'locked')
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 51', {'timer_s': 90, 'events': [[90, 'berth_occ'], [150, 'berth_clr'], [195, 'query'], [255, 'berth_occ'], [315, 'query'], [320, 'query'], [320, 'overlap_occ'], [440, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 18', {'timer_s': 90, 'events': [[0, 'query'], [0, 'query'], [30, 'berth_occ'], [120, 'overlap_occ'], [210, 'berth_clr'], [215, 'query'], [245, 'berth_occ'], [365, 'query']]}, ['locked', 'locked', 'released', 'released']), ('boundary: expiry exactly on time', {'timer_s': 60, 'events': [[10, 'berth_occ'], [70, 'query']]}, ['released']), ('control 1', {'timer_s': 45, 'events': [[5, 'overlap_occ'], [35, 'query'], [65, 'berth_clr'], [125, 'query'], [170, 'query'], [170, 'berth_clr'], [230, 'berth_occ'], [350, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 4', {'timer_s': 90, 'events': [[60, 'berth_clr'], [150, 'berth_occ'], [155, 'berth_occ'], [155, 'query']]}, ['locked']), ('control 7', {'timer_s': 45, 'events': [[5, 'query'], [65, 'overlap_occ'], [110, 'overlap_occ'], [170, 'query']]}, ['locked', 'locked'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('control 59', {'timer_s': 45, 'events': [[30, 'query'], [120, 'query'], [120, 'berth_occ'], [210, 'query'], [215, 'berth_clr'], [215, 'berth_clr'], [215, 'berth_clr'], [275, 'query']]}, ['locked', 'locked', 'released', 'released']), ('boundary: train stops at time zero', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_occ'], [60, 'query']]}, ['released']), ('boundary: overrun into the overlap', {'timer_s': 60, 'events': [[0, 'berth_occ'], [20, 'overlap_occ'], [120, 'query']]}, ['locked']), ('control 12', {'timer_s': 120, 'events': [[60, 'berth_occ'], [65, 'query'], [70, 'query'], [70, 'query'], [75, 'berth_occ'], [80, 'berth_occ'], [125, 'berth_clr'], [125, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 15', {'timer_s': 120, 'events': [[60, 'berth_clr'], [105, 'berth_clr'], [110, 'berth_clr'], [115, 'berth_clr'], [175, 'query'], [175, 'berth_clr'], [235, 'query'], [265, 'overlap_occ'], [270, 'berth_clr'], [390, 'query']]}, ['locked', 'locked', 'locked']), ('control 18', {'timer_s': 90, 'events': [[0, 'query'], [0, 'query'], [30, 'berth_occ'], [120, 'overlap_occ'], [210, 'berth_clr'], [215, 'query'], [245, 'berth_occ'], [365, 'query']]}, ['locked', 'locked', 'released', 'released'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 9', {'timer_s': 60, 'events': [[5, 'berth_occ'], [5, 'query'], [35, 'berth_clr'], [155, 'query']]}, ['locked', 'locked']), ('control 78', {'timer_s': 90, 'events': [[0, 'query'], [90, 'berth_occ'], [120, 'berth_occ'], [120, 'query'], [210, 'berth_clr'], [210, 'query']]}, ['locked', 'locked', 'released']), ('boundary: overrun into the overlap', {'timer_s': 60, 'events': [[0, 'berth_occ'], [20, 'overlap_occ'], [120, 'query']]}, ['locked']), ('control 23', {'timer_s': 45, 'events': [[0, 'query'], [5, 'berth_occ'], [95, 'berth_occ'], [185, 'berth_occ'], [245, 'query']]}, ['locked', 'released']), ('control 26', {'timer_s': 60, 'events': [[30, 'query'], [60, 'query'], [150, 'overlap_occ'], [150, 'query']]}, ['locked', 'locked', 'locked']), ('control 29', {'timer_s': 90, 'events': [[90, 'overlap_occ'], [95, 'query'], [95, 'berth_occ'], [185, 'query'], [230, 'query'], [260, 'query'], [350, 'berth_occ'], [410, 'query']]}, ['locked', 'locked', 'locked', 'locked', 'locked'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 75', {'timer_s': 90, 'events': [[0, 'berth_occ'], [0, 'query'], [60, 'berth_clr'], [120, 'query'], [180, 'overlap_occ'], [225, 'berth_occ'], [270, 'query'], [275, 'berth_occ'], [320, 'overlap_occ'], [380, 'berth_occ'], [380, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 33', {'timer_s': 60, 'events': [[60, 'berth_occ'], [60, 'query'], [120, 'query'], [150, 'berth_occ'], [240, 'berth_clr'], [360, 'query']]}, ['locked', 'released', 'released']), ('boundary: ninety second timer at one minute', {'timer_s': 90, 'events': [[0, 'berth_occ'], [60, 'query'], [89, 'query'], [90, 'query']]}, ['locked', 'locked', 'released']), ('control 34', {'timer_s': 60, 'events': [[5, 'query'], [35, 'query'], [80, 'berth_occ'], [170, 'berth_occ'], [260, 'berth_occ'], [320, 'berth_occ'], [350, 'overlap_occ'], [395, 'overlap_occ'], [440, 'query'], [500, 'query'], [560, 'query']]}, ['locked', 'locked', 'released', 'released', 'released']), ('control 37', {'timer_s': 120, 'events': [[30, 'query'], [60, 'overlap_occ'], [120, 'berth_occ'], [180, 'overlap_occ'], [185, 'overlap_occ'], [185, 'overlap_occ'], [245, 'query'], [275, 'query'], [280, 'overlap_occ'], [280, 'berth_occ'], [280, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 40', {'timer_s': 90, 'events': [[60, 'overlap_occ'], [90, 'query'], [135, 'berth_occ'], [195, 'overlap_occ'], [225, 'berth_occ'], [230, 'berth_clr'], [230, 'query']]}, ['locked', 'locked'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 8', {'timer_s': 120, 'events': [[30, 'berth_occ'], [120, 'berth_clr'], [165, 'berth_clr'], [170, 'berth_occ'], [215, 'berth_clr'], [215, 'overlap_occ'], [305, 'query'], [305, 'berth_occ'], [395, 'berth_occ'], [440, 'berth_occ'], [560, 'query']]}, ['locked', 'locked']), ('control 66', {'timer_s': 90, 'events': [[5, 'query'], [65, 'berth_occ'], [155, 'overlap_occ'], [160, 'overlap_occ'], [160, 'berth_occ'], [165, 'berth_occ'], [210, 'berth_occ'], [210, 'berth_clr'], [215, 'overlap_occ'], [275, 'overlap_occ'], [275, 'query']]}, ['locked', 'released']), ('boundary: expiry exactly on time', {'timer_s': 60, 'events': [[10, 'berth_occ'], [70, 'query']]}, ['released']), ('control 45', {'timer_s': 60, 'events': [[60, 'query'], [120, 'query'], [150, 'overlap_occ'], [155, 'berth_occ'], [245, 'overlap_occ'], [290, 'berth_occ'], [380, 'berth_clr'], [470, 'overlap_occ'], [470, 'query'], [475, 'berth_occ'], [595, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 48', {'timer_s': 45, 'events': [[60, 'overlap_occ'], [150, 'berth_occ'], [180, 'overlap_occ'], [180, 'berth_occ'], [270, 'berth_clr'], [275, 'berth_clr'], [275, 'overlap_occ'], [275, 'query']]}, ['locked']), ('sampled regression 51', {'timer_s': 90, 'events': [[90, 'berth_occ'], [150, 'berth_clr'], [195, 'query'], [255, 'berth_occ'], [315, 'query'], [320, 'query'], [320, 'overlap_occ'], [440, 'query']]}, ['locked', 'locked', 'locked', 'locked'])]]
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: train leaves before expiry | ['locked'] | ['locked'] | Passed |
| boundary: berth clears after release | ['released', 'locked'] | ['released', 'released'] | Failed |
| sampled regression 51 | ['locked', 'locked', 'locked', 'locked'] | ['locked', 'locked', 'locked', 'locked'] | Passed |
| control 18 | ['locked', 'locked', 'locked', 'released'] | ['locked', 'locked', 'released', 'released'] | Failed |
| boundary: expiry exactly on time | ['released'] | ['released'] | Passed |
| control 1 | ['locked', 'locked', 'locked', 'locked'] | ['locked', 'locked', 'locked', 'locked'] | Passed |
| control 4 | ['locked'] | ['locked'] | Passed |
| control 7 | ['locked', 'locked'] | ['locked', 'locked'] | Passed |
SHA-256 / 4e1a345dbc762d706241877ec453b59312e5840fadba7b27f95d0be92f7bac20
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(x):
T = x['timer_s']
start = None
overran = False
released = False
out = []
for t, ev in x['events']:
if start is not None and not released and not overran and t - start >= T:
released = True
if ev == 'berth_occ':
if start is None:
start = t
elif ev == 'berth_clr':
if not released:
start = None
elif ev == 'overlap_occ':
if not released:
overran = True
elif ev == 'query':
out.append('released' if released else 'locked')
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 51', {'timer_s': 90, 'events': [[90, 'berth_occ'], [150, 'berth_clr'], [195, 'query'], [255, 'berth_occ'], [315, 'query'], [320, 'query'], [320, 'overlap_occ'], [440, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 18', {'timer_s': 90, 'events': [[0, 'query'], [0, 'query'], [30, 'berth_occ'], [120, 'overlap_occ'], [210, 'berth_clr'], [215, 'query'], [245, 'berth_occ'], [365, 'query']]}, ['locked', 'locked', 'released', 'released']), ('boundary: expiry exactly on time', {'timer_s': 60, 'events': [[10, 'berth_occ'], [70, 'query']]}, ['released']), ('control 1', {'timer_s': 45, 'events': [[5, 'overlap_occ'], [35, 'query'], [65, 'berth_clr'], [125, 'query'], [170, 'query'], [170, 'berth_clr'], [230, 'berth_occ'], [350, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 4', {'timer_s': 90, 'events': [[60, 'berth_clr'], [150, 'berth_occ'], [155, 'berth_occ'], [155, 'query']]}, ['locked']), ('control 7', {'timer_s': 45, 'events': [[5, 'query'], [65, 'overlap_occ'], [110, 'overlap_occ'], [170, 'query']]}, ['locked', 'locked'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('control 59', {'timer_s': 45, 'events': [[30, 'query'], [120, 'query'], [120, 'berth_occ'], [210, 'query'], [215, 'berth_clr'], [215, 'berth_clr'], [215, 'berth_clr'], [275, 'query']]}, ['locked', 'locked', 'released', 'released']), ('boundary: train stops at time zero', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_occ'], [60, 'query']]}, ['released']), ('boundary: overrun into the overlap', {'timer_s': 60, 'events': [[0, 'berth_occ'], [20, 'overlap_occ'], [120, 'query']]}, ['locked']), ('control 12', {'timer_s': 120, 'events': [[60, 'berth_occ'], [65, 'query'], [70, 'query'], [70, 'query'], [75, 'berth_occ'], [80, 'berth_occ'], [125, 'berth_clr'], [125, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 15', {'timer_s': 120, 'events': [[60, 'berth_clr'], [105, 'berth_clr'], [110, 'berth_clr'], [115, 'berth_clr'], [175, 'query'], [175, 'berth_clr'], [235, 'query'], [265, 'overlap_occ'], [270, 'berth_clr'], [390, 'query']]}, ['locked', 'locked', 'locked']), ('control 18', {'timer_s': 90, 'events': [[0, 'query'], [0, 'query'], [30, 'berth_occ'], [120, 'overlap_occ'], [210, 'berth_clr'], [215, 'query'], [245, 'berth_occ'], [365, 'query']]}, ['locked', 'locked', 'released', 'released'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 9', {'timer_s': 60, 'events': [[5, 'berth_occ'], [5, 'query'], [35, 'berth_clr'], [155, 'query']]}, ['locked', 'locked']), ('control 78', {'timer_s': 90, 'events': [[0, 'query'], [90, 'berth_occ'], [120, 'berth_occ'], [120, 'query'], [210, 'berth_clr'], [210, 'query']]}, ['locked', 'locked', 'released']), ('boundary: overrun into the overlap', {'timer_s': 60, 'events': [[0, 'berth_occ'], [20, 'overlap_occ'], [120, 'query']]}, ['locked']), ('control 23', {'timer_s': 45, 'events': [[0, 'query'], [5, 'berth_occ'], [95, 'berth_occ'], [185, 'berth_occ'], [245, 'query']]}, ['locked', 'released']), ('control 26', {'timer_s': 60, 'events': [[30, 'query'], [60, 'query'], [150, 'overlap_occ'], [150, 'query']]}, ['locked', 'locked', 'locked']), ('control 29', {'timer_s': 90, 'events': [[90, 'overlap_occ'], [95, 'query'], [95, 'berth_occ'], [185, 'query'], [230, 'query'], [260, 'query'], [350, 'berth_occ'], [410, 'query']]}, ['locked', 'locked', 'locked', 'locked', 'locked'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 75', {'timer_s': 90, 'events': [[0, 'berth_occ'], [0, 'query'], [60, 'berth_clr'], [120, 'query'], [180, 'overlap_occ'], [225, 'berth_occ'], [270, 'query'], [275, 'berth_occ'], [320, 'overlap_occ'], [380, 'berth_occ'], [380, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 33', {'timer_s': 60, 'events': [[60, 'berth_occ'], [60, 'query'], [120, 'query'], [150, 'berth_occ'], [240, 'berth_clr'], [360, 'query']]}, ['locked', 'released', 'released']), ('boundary: ninety second timer at one minute', {'timer_s': 90, 'events': [[0, 'berth_occ'], [60, 'query'], [89, 'query'], [90, 'query']]}, ['locked', 'locked', 'released']), ('control 34', {'timer_s': 60, 'events': [[5, 'query'], [35, 'query'], [80, 'berth_occ'], [170, 'berth_occ'], [260, 'berth_occ'], [320, 'berth_occ'], [350, 'overlap_occ'], [395, 'overlap_occ'], [440, 'query'], [500, 'query'], [560, 'query']]}, ['locked', 'locked', 'released', 'released', 'released']), ('control 37', {'timer_s': 120, 'events': [[30, 'query'], [60, 'overlap_occ'], [120, 'berth_occ'], [180, 'overlap_occ'], [185, 'overlap_occ'], [185, 'overlap_occ'], [245, 'query'], [275, 'query'], [280, 'overlap_occ'], [280, 'berth_occ'], [280, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 40', {'timer_s': 90, 'events': [[60, 'overlap_occ'], [90, 'query'], [135, 'berth_occ'], [195, 'overlap_occ'], [225, 'berth_occ'], [230, 'berth_clr'], [230, 'query']]}, ['locked', 'locked'])], [('regression: train leaves before expiry', {'timer_s': 60, 'events': [[0, 'berth_occ'], [30, 'berth_clr'], [90, 'query']]}, ['locked']), ('boundary: berth clears after release', {'timer_s': 60, 'events': [[0, 'berth_occ'], [60, 'query'], [65, 'berth_clr'], [70, 'query']]}, ['released', 'released']), ('sampled regression 8', {'timer_s': 120, 'events': [[30, 'berth_occ'], [120, 'berth_clr'], [165, 'berth_clr'], [170, 'berth_occ'], [215, 'berth_clr'], [215, 'overlap_occ'], [305, 'query'], [305, 'berth_occ'], [395, 'berth_occ'], [440, 'berth_occ'], [560, 'query']]}, ['locked', 'locked']), ('control 66', {'timer_s': 90, 'events': [[5, 'query'], [65, 'berth_occ'], [155, 'overlap_occ'], [160, 'overlap_occ'], [160, 'berth_occ'], [165, 'berth_occ'], [210, 'berth_occ'], [210, 'berth_clr'], [215, 'overlap_occ'], [275, 'overlap_occ'], [275, 'query']]}, ['locked', 'released']), ('boundary: expiry exactly on time', {'timer_s': 60, 'events': [[10, 'berth_occ'], [70, 'query']]}, ['released']), ('control 45', {'timer_s': 60, 'events': [[60, 'query'], [120, 'query'], [150, 'overlap_occ'], [155, 'berth_occ'], [245, 'overlap_occ'], [290, 'berth_occ'], [380, 'berth_clr'], [470, 'overlap_occ'], [470, 'query'], [475, 'berth_occ'], [595, 'query']]}, ['locked', 'locked', 'locked', 'locked']), ('control 48', {'timer_s': 45, 'events': [[60, 'overlap_occ'], [150, 'berth_occ'], [180, 'overlap_occ'], [180, 'berth_occ'], [270, 'berth_clr'], [275, 'berth_clr'], [275, 'overlap_occ'], [275, 'query']]}, ['locked']), ('sampled regression 51', {'timer_s': 90, 'events': [[90, 'berth_occ'], [150, 'berth_clr'], [195, 'query'], [255, 'berth_occ'], [315, 'query'], [320, 'query'], [320, 'overlap_occ'], [440, 'query']]}, ['locked', 'locked', 'locked', 'locked'])]]
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: train leaves before expiry | ['locked'] | ['locked'] | Passed |
| boundary: berth clears after release | ['released', 'released'] | ['released', 'released'] | Passed |
| sampled regression 51 | ['locked', 'locked', 'locked', 'locked'] | ['locked', 'locked', 'locked', 'locked'] | Passed |
| control 18 | ['locked', 'locked', 'released', 'released'] | ['locked', 'locked', 'released', 'released'] | Passed |
| boundary: expiry exactly on time | ['released'] | ['released'] | Passed |
| control 1 | ['locked', 'locked', 'locked', 'locked'] | ['locked', 'locked', 'locked', 'locked'] | Passed |
| control 4 | ['locked'] | ['locked'] | Passed |
| control 7 | ['locked', 'locked'] | ['locked', 'locked'] | Passed |
SHA-256 / 645f0623977b43ead103bc5a0baeae889f40f5bcc16142a355d3c9bfb49da40a
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:49.188485+00:00.
Case digest / 95fb442797ecc8c770510d6dabe85f103b8cae60908f4b351b8e13472f9f18e1