FA-66916 / Railway interlocking logic / Open access
Approach locking time release: release deadline evaluation · case 01
An approach-locked route stays locked at the instant its timer expires.
ROOT CAUSE
The expiry comparison is strict, so an event exactly at the deadline still sees the lock.
VERIFIED REPAIR
Release the lock at the first event whose time reaches the deadline, before handling that event.
Unsuccessful approach: Checking the timer only on queries refuses a route set at or after the deadline until someone queries.
Case contract
A route can be set only when free. pass_signal moves a set route to in-use; train_clear frees an in-use route. Cancelling a set route frees it at once unless a train is in the approach section, in which case it is approach-locked until cancel time + release_s (released when an event time reaches the deadline). approach_occ/approach_clear track the approach section. query appends set, free, in-use or locked-until:<t>.
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['release_s']
state = 'free'
until = None
approach = False
out = []
for t, kind in x['events']:
if state == 'locked' and t > until:
state = 'free'
if kind == 'approach_occ':
approach = True
elif kind == 'approach_clear':
approach = False
elif kind == 'set' and state == 'free':
state = 'set'
elif kind == 'cancel' and state == 'set':
if approach:
state = 'locked'
until = t + T
else:
state = 'free'
elif kind == 'pass_signal':
approach = False
if state == 'set':
state = 'in-use'
elif kind == 'train_clear' and state == 'in-use':
state = 'free'
elif kind == 'query':
out.append('locked-until:%d' % until if state == 'locked' else state)
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('boundary: train backs out of the approach', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'approach_clear'], [2, 'set'], [3, 'cancel'], [4, 'query']]}, ['free']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('control 1', {'release_s': 120, 'events': [[120, 'query'], [125, 'set'], [185, 'set'], [215, 'pass_signal'], [275, 'query'], [475, 'query']]}, ['free', 'in-use', 'in-use']), ('control 4', {'release_s': 60, 'events': [[30, 'query'], [60, 'query'], [120, 'query'], [180, 'cancel'], [240, 'query'], [245, 'approach_occ'], [445, 'query']]}, ['free', 'free', 'free', 'free', 'free']), ('control 7', {'release_s': 120, 'events': [[0, 'cancel'], [0, 'query'], [0, 'approach_occ'], [1, 'set'], [11, 'approach_clear'], [41, 'query'], [42, 'approach_occ'], [242, 'query']]}, ['free', 'set', 'set'])], [('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('boundary: train backs out of the approach', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'approach_clear'], [2, 'set'], [3, 'cancel'], [4, 'query']]}, ['free']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('control 12', {'release_s': 120, 'events': [[1, 'query'], [121, 'approach_clear'], [241, 'set'], [271, 'set'], [391, 'approach_occ'], [451, 'query']]}, ['free', 'set']), ('control 15', {'release_s': 60, 'events': [[5, 'set'], [6, 'query'], [6, 'cancel'], [36, 'set'], [46, 'query'], [106, 'approach_clear'], [226, 'query'], [227, 'query'], [237, 'query'], [267, 'set'], [327, 'set'], [327, 'query']]}, ['set', 'set', 'set', 'set', 'set', 'set']), ('control 18', {'release_s': 60, 'events': [[5, 'approach_occ'], [10, 'approach_clear'], [70, 'approach_clear'], [190, 'query'], [195, 'set'], [195, 'cancel'], [195, 'cancel'], [200, 'query'], [260, 'set'], [265, 'set'], [325, 'query']]}, ['free', 'free', 'set'])], [('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('control 57', {'release_s': 120, 'events': [[0, 'train_clear'], [10, 'set'], [10, 'query'], [15, 'approach_occ'], [15, 'set'], [16, 'train_clear'], [46, 'query'], [56, 'cancel'], [66, 'set'], [126, 'set'], [186, 'set'], [196, 'train_clear'], [196, 'query']]}, ['set', 'set', 'set']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('boundary: set with a train approaching', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'set'], [2, 'query']]}, ['set']), ('control 23', {'release_s': 60, 'events': [[10, 'cancel'], [15, 'set'], [25, 'approach_occ'], [26, 'set'], [36, 'cancel'], [156, 'query']]}, ['free']), ('control 26', {'release_s': 60, 'events': [[1, 'approach_occ'], [6, 'set'], [66, 'set'], [66, 'cancel'], [96, 'query'], [106, 'approach_clear'], [136, 'query'], [141, 'approach_clear'], [151, 'approach_occ'], [211, 'train_clear'], [271, 'query']]}, ['locked-until:126', 'free', 'free']), ('control 29', {'release_s': 60, 'events': [[0, 'set'], [0, 'set'], [30, 'train_clear'], [40, 'set'], [40, 'query'], [100, 'cancel'], [110, 'approach_occ'], [170, 'query']]}, ['set', 'free'])], [('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('boundary: cancel with empty approach', {'release_s': 60, 'events': [[0, 'set'], [1, 'cancel'], [2, 'query']]}, ['free']), ('boundary: set attempted while locked', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [30, 'set'], [31, 'query']]}, ['locked-until:62']), ('control 34', {'release_s': 120, 'events': [[120, 'set'], [121, 'set'], [121, 'cancel'], [241, 'approach_occ'], [361, 'pass_signal'], [371, 'cancel'], [491, 'approach_occ'], [611, 'query']]}, ['free']), ('control 37', {'release_s': 60, 'events': [[60, 'query'], [61, 'train_clear'], [71, 'set'], [131, 'train_clear'], [131, 'pass_signal'], [136, 'approach_occ'], [196, 'set'], [197, 'cancel'], [202, 'set'], [262, 'train_clear'], [382, 'query'], [382, 'query']]}, ['free', 'free', 'free']), ('control 40', {'release_s': 120, 'events': [[0, 'query'], [30, 'cancel'], [90, 'approach_occ'], [100, 'set'], [130, 'query'], [135, 'approach_clear'], [255, 'train_clear'], [260, 'query'], [265, 'approach_occ'], [270, 'set'], [275, 'train_clear'], [305, 'cancel'], [365, 'query']]}, ['free', 'set', 'set', 'locked-until:425'])], [('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: train backs out of the approach', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'approach_clear'], [2, 'set'], [3, 'cancel'], [4, 'query']]}, ['free']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('control 45', {'release_s': 120, 'events': [[0, 'set'], [0, 'cancel'], [0, 'train_clear'], [0, 'approach_occ'], [1, 'approach_clear'], [6, 'approach_clear'], [126, 'query'], [136, 'set'], [141, 'train_clear'], [151, 'cancel'], [152, 'approach_clear'], [152, 'pass_signal'], [212, 'query']]}, ['free', 'free']), ('control 48', {'release_s': 60, 'events': [[120, 'set'], [121, 'train_clear'], [122, 'set'], [242, 'query'], [242, 'query'], [252, 'pass_signal'], [257, 'approach_occ'], [257, 'query']]}, ['set', 'set', 'in-use']), ('control 51', {'release_s': 60, 'events': [[120, 'pass_signal'], [120, 'cancel'], [125, 'approach_clear'], [126, 'cancel'], [136, 'cancel'], [256, 'approach_clear'], [316, 'pass_signal'], [376, 'query'], [377, 'query'], [387, 'cancel'], [387, 'query']]}, ['free', 'free', 'free'])]]
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: query at exactly the release time | ['locked-until:130'] | ['free'] | Failed |
| regression: re-set at exactly the release time | ['free'] | ['set'] | Failed |
| boundary: second lock after an earlier one | ['locked-until:140'] | ['locked-until:140'] | Passed |
| boundary: train backs out of the approach | ['free'] | ['free'] | Passed |
| boundary: cancel under a train | ['in-use', 'free'] | ['in-use', 'free'] | Passed |
| control 1 | ['free', 'in-use', 'in-use'] | ['free', 'in-use', 'in-use'] | Passed |
| control 4 | ['free', 'free', 'free', 'free', 'free'] | ['free', 'free', 'free', 'free', 'free'] | Passed |
| control 7 | ['free', 'set', 'set'] | ['free', 'set', 'set'] | Passed |
SHA-256 / 445a1b2a677b5d3aa8f2b2ded9886ec47f51cb882e4126a26d73c675c3c79ecf
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(x):
T = x['release_s']
state = 'free'
until = None
approach = False
out = []
for t, kind in x['events']:
if kind == 'approach_occ':
approach = True
elif kind == 'approach_clear':
approach = False
elif kind == 'set' and state == 'free':
state = 'set'
elif kind == 'cancel' and state == 'set':
if approach:
state = 'locked'
until = t + T
else:
state = 'free'
elif kind == 'pass_signal':
approach = False
if state == 'set':
state = 'in-use'
elif kind == 'train_clear' and state == 'in-use':
state = 'free'
elif kind == 'query':
if state == 'locked' and t >= until:
state = 'free'
out.append('locked-until:%d' % until if state == 'locked' else state)
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('boundary: train backs out of the approach', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'approach_clear'], [2, 'set'], [3, 'cancel'], [4, 'query']]}, ['free']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('control 1', {'release_s': 120, 'events': [[120, 'query'], [125, 'set'], [185, 'set'], [215, 'pass_signal'], [275, 'query'], [475, 'query']]}, ['free', 'in-use', 'in-use']), ('control 4', {'release_s': 60, 'events': [[30, 'query'], [60, 'query'], [120, 'query'], [180, 'cancel'], [240, 'query'], [245, 'approach_occ'], [445, 'query']]}, ['free', 'free', 'free', 'free', 'free']), ('control 7', {'release_s': 120, 'events': [[0, 'cancel'], [0, 'query'], [0, 'approach_occ'], [1, 'set'], [11, 'approach_clear'], [41, 'query'], [42, 'approach_occ'], [242, 'query']]}, ['free', 'set', 'set'])], [('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('boundary: train backs out of the approach', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'approach_clear'], [2, 'set'], [3, 'cancel'], [4, 'query']]}, ['free']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('control 12', {'release_s': 120, 'events': [[1, 'query'], [121, 'approach_clear'], [241, 'set'], [271, 'set'], [391, 'approach_occ'], [451, 'query']]}, ['free', 'set']), ('control 15', {'release_s': 60, 'events': [[5, 'set'], [6, 'query'], [6, 'cancel'], [36, 'set'], [46, 'query'], [106, 'approach_clear'], [226, 'query'], [227, 'query'], [237, 'query'], [267, 'set'], [327, 'set'], [327, 'query']]}, ['set', 'set', 'set', 'set', 'set', 'set']), ('control 18', {'release_s': 60, 'events': [[5, 'approach_occ'], [10, 'approach_clear'], [70, 'approach_clear'], [190, 'query'], [195, 'set'], [195, 'cancel'], [195, 'cancel'], [200, 'query'], [260, 'set'], [265, 'set'], [325, 'query']]}, ['free', 'free', 'set'])], [('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('control 57', {'release_s': 120, 'events': [[0, 'train_clear'], [10, 'set'], [10, 'query'], [15, 'approach_occ'], [15, 'set'], [16, 'train_clear'], [46, 'query'], [56, 'cancel'], [66, 'set'], [126, 'set'], [186, 'set'], [196, 'train_clear'], [196, 'query']]}, ['set', 'set', 'set']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('boundary: set with a train approaching', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'set'], [2, 'query']]}, ['set']), ('control 23', {'release_s': 60, 'events': [[10, 'cancel'], [15, 'set'], [25, 'approach_occ'], [26, 'set'], [36, 'cancel'], [156, 'query']]}, ['free']), ('control 26', {'release_s': 60, 'events': [[1, 'approach_occ'], [6, 'set'], [66, 'set'], [66, 'cancel'], [96, 'query'], [106, 'approach_clear'], [136, 'query'], [141, 'approach_clear'], [151, 'approach_occ'], [211, 'train_clear'], [271, 'query']]}, ['locked-until:126', 'free', 'free']), ('control 29', {'release_s': 60, 'events': [[0, 'set'], [0, 'set'], [30, 'train_clear'], [40, 'set'], [40, 'query'], [100, 'cancel'], [110, 'approach_occ'], [170, 'query']]}, ['set', 'free'])], [('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('boundary: cancel with empty approach', {'release_s': 60, 'events': [[0, 'set'], [1, 'cancel'], [2, 'query']]}, ['free']), ('boundary: set attempted while locked', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [30, 'set'], [31, 'query']]}, ['locked-until:62']), ('control 34', {'release_s': 120, 'events': [[120, 'set'], [121, 'set'], [121, 'cancel'], [241, 'approach_occ'], [361, 'pass_signal'], [371, 'cancel'], [491, 'approach_occ'], [611, 'query']]}, ['free']), ('control 37', {'release_s': 60, 'events': [[60, 'query'], [61, 'train_clear'], [71, 'set'], [131, 'train_clear'], [131, 'pass_signal'], [136, 'approach_occ'], [196, 'set'], [197, 'cancel'], [202, 'set'], [262, 'train_clear'], [382, 'query'], [382, 'query']]}, ['free', 'free', 'free']), ('control 40', {'release_s': 120, 'events': [[0, 'query'], [30, 'cancel'], [90, 'approach_occ'], [100, 'set'], [130, 'query'], [135, 'approach_clear'], [255, 'train_clear'], [260, 'query'], [265, 'approach_occ'], [270, 'set'], [275, 'train_clear'], [305, 'cancel'], [365, 'query']]}, ['free', 'set', 'set', 'locked-until:425'])], [('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: train backs out of the approach', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'approach_clear'], [2, 'set'], [3, 'cancel'], [4, 'query']]}, ['free']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('control 45', {'release_s': 120, 'events': [[0, 'set'], [0, 'cancel'], [0, 'train_clear'], [0, 'approach_occ'], [1, 'approach_clear'], [6, 'approach_clear'], [126, 'query'], [136, 'set'], [141, 'train_clear'], [151, 'cancel'], [152, 'approach_clear'], [152, 'pass_signal'], [212, 'query']]}, ['free', 'free']), ('control 48', {'release_s': 60, 'events': [[120, 'set'], [121, 'train_clear'], [122, 'set'], [242, 'query'], [242, 'query'], [252, 'pass_signal'], [257, 'approach_occ'], [257, 'query']]}, ['set', 'set', 'in-use']), ('control 51', {'release_s': 60, 'events': [[120, 'pass_signal'], [120, 'cancel'], [125, 'approach_clear'], [126, 'cancel'], [136, 'cancel'], [256, 'approach_clear'], [316, 'pass_signal'], [376, 'query'], [377, 'query'], [387, 'cancel'], [387, 'query']]}, ['free', 'free', 'free'])]]
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: query at exactly the release time | ['free'] | ['free'] | Passed |
| regression: re-set at exactly the release time | ['free'] | ['set'] | Failed |
| boundary: second lock after an earlier one | ['free'] | ['locked-until:140'] | Failed |
| boundary: train backs out of the approach | ['free'] | ['free'] | Passed |
| boundary: cancel under a train | ['in-use', 'free'] | ['in-use', 'free'] | Passed |
| control 1 | ['free', 'in-use', 'in-use'] | ['free', 'in-use', 'in-use'] | Passed |
| control 4 | ['free', 'free', 'free', 'free', 'free'] | ['free', 'free', 'free', 'free', 'free'] | Passed |
| control 7 | ['free', 'set', 'set'] | ['free', 'set', 'set'] | Passed |
SHA-256 / 4851c04f3d350244c535a9ab098caf9fe7e7cbced67045fbd75e1ed646e3aef8
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(x):
T = x['release_s']
state = 'free'
until = None
approach = False
out = []
for t, kind in x['events']:
if state == 'locked' and t >= until:
state = 'free'
if kind == 'approach_occ':
approach = True
elif kind == 'approach_clear':
approach = False
elif kind == 'set' and state == 'free':
state = 'set'
elif kind == 'cancel' and state == 'set':
if approach:
state = 'locked'
until = t + T
else:
state = 'free'
elif kind == 'pass_signal':
approach = False
if state == 'set':
state = 'in-use'
elif kind == 'train_clear' and state == 'in-use':
state = 'free'
elif kind == 'query':
out.append('locked-until:%d' % until if state == 'locked' else state)
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('boundary: train backs out of the approach', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'approach_clear'], [2, 'set'], [3, 'cancel'], [4, 'query']]}, ['free']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('control 1', {'release_s': 120, 'events': [[120, 'query'], [125, 'set'], [185, 'set'], [215, 'pass_signal'], [275, 'query'], [475, 'query']]}, ['free', 'in-use', 'in-use']), ('control 4', {'release_s': 60, 'events': [[30, 'query'], [60, 'query'], [120, 'query'], [180, 'cancel'], [240, 'query'], [245, 'approach_occ'], [445, 'query']]}, ['free', 'free', 'free', 'free', 'free']), ('control 7', {'release_s': 120, 'events': [[0, 'cancel'], [0, 'query'], [0, 'approach_occ'], [1, 'set'], [11, 'approach_clear'], [41, 'query'], [42, 'approach_occ'], [242, 'query']]}, ['free', 'set', 'set'])], [('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('boundary: train backs out of the approach', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'approach_clear'], [2, 'set'], [3, 'cancel'], [4, 'query']]}, ['free']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('control 12', {'release_s': 120, 'events': [[1, 'query'], [121, 'approach_clear'], [241, 'set'], [271, 'set'], [391, 'approach_occ'], [451, 'query']]}, ['free', 'set']), ('control 15', {'release_s': 60, 'events': [[5, 'set'], [6, 'query'], [6, 'cancel'], [36, 'set'], [46, 'query'], [106, 'approach_clear'], [226, 'query'], [227, 'query'], [237, 'query'], [267, 'set'], [327, 'set'], [327, 'query']]}, ['set', 'set', 'set', 'set', 'set', 'set']), ('control 18', {'release_s': 60, 'events': [[5, 'approach_occ'], [10, 'approach_clear'], [70, 'approach_clear'], [190, 'query'], [195, 'set'], [195, 'cancel'], [195, 'cancel'], [200, 'query'], [260, 'set'], [265, 'set'], [325, 'query']]}, ['free', 'free', 'set'])], [('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('control 57', {'release_s': 120, 'events': [[0, 'train_clear'], [10, 'set'], [10, 'query'], [15, 'approach_occ'], [15, 'set'], [16, 'train_clear'], [46, 'query'], [56, 'cancel'], [66, 'set'], [126, 'set'], [186, 'set'], [196, 'train_clear'], [196, 'query']]}, ['set', 'set', 'set']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('boundary: set with a train approaching', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'set'], [2, 'query']]}, ['set']), ('control 23', {'release_s': 60, 'events': [[10, 'cancel'], [15, 'set'], [25, 'approach_occ'], [26, 'set'], [36, 'cancel'], [156, 'query']]}, ['free']), ('control 26', {'release_s': 60, 'events': [[1, 'approach_occ'], [6, 'set'], [66, 'set'], [66, 'cancel'], [96, 'query'], [106, 'approach_clear'], [136, 'query'], [141, 'approach_clear'], [151, 'approach_occ'], [211, 'train_clear'], [271, 'query']]}, ['locked-until:126', 'free', 'free']), ('control 29', {'release_s': 60, 'events': [[0, 'set'], [0, 'set'], [30, 'train_clear'], [40, 'set'], [40, 'query'], [100, 'cancel'], [110, 'approach_occ'], [170, 'query']]}, ['set', 'free'])], [('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('boundary: cancel with empty approach', {'release_s': 60, 'events': [[0, 'set'], [1, 'cancel'], [2, 'query']]}, ['free']), ('boundary: set attempted while locked', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [30, 'set'], [31, 'query']]}, ['locked-until:62']), ('control 34', {'release_s': 120, 'events': [[120, 'set'], [121, 'set'], [121, 'cancel'], [241, 'approach_occ'], [361, 'pass_signal'], [371, 'cancel'], [491, 'approach_occ'], [611, 'query']]}, ['free']), ('control 37', {'release_s': 60, 'events': [[60, 'query'], [61, 'train_clear'], [71, 'set'], [131, 'train_clear'], [131, 'pass_signal'], [136, 'approach_occ'], [196, 'set'], [197, 'cancel'], [202, 'set'], [262, 'train_clear'], [382, 'query'], [382, 'query']]}, ['free', 'free', 'free']), ('control 40', {'release_s': 120, 'events': [[0, 'query'], [30, 'cancel'], [90, 'approach_occ'], [100, 'set'], [130, 'query'], [135, 'approach_clear'], [255, 'train_clear'], [260, 'query'], [265, 'approach_occ'], [270, 'set'], [275, 'train_clear'], [305, 'cancel'], [365, 'query']]}, ['free', 'set', 'set', 'locked-until:425'])], [('regression: query at exactly the release time', {'release_s': 120, 'events': [[0, 'set'], [5, 'approach_occ'], [10, 'cancel'], [130, 'query']]}, ['free']), ('regression: re-set at exactly the release time', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [62, 'set'], [63, 'query']]}, ['set']), ('boundary: train backs out of the approach', {'release_s': 60, 'events': [[0, 'approach_occ'], [1, 'approach_clear'], [2, 'set'], [3, 'cancel'], [4, 'query']]}, ['free']), ('boundary: second lock after an earlier one', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'cancel'], [70, 'set'], [80, 'cancel'], [81, 'query']]}, ['locked-until:140']), ('boundary: cancel under a train', {'release_s': 60, 'events': [[0, 'set'], [1, 'approach_occ'], [2, 'pass_signal'], [3, 'cancel'], [4, 'query'], [5, 'train_clear'], [6, 'query']]}, ['in-use', 'free']), ('control 45', {'release_s': 120, 'events': [[0, 'set'], [0, 'cancel'], [0, 'train_clear'], [0, 'approach_occ'], [1, 'approach_clear'], [6, 'approach_clear'], [126, 'query'], [136, 'set'], [141, 'train_clear'], [151, 'cancel'], [152, 'approach_clear'], [152, 'pass_signal'], [212, 'query']]}, ['free', 'free']), ('control 48', {'release_s': 60, 'events': [[120, 'set'], [121, 'train_clear'], [122, 'set'], [242, 'query'], [242, 'query'], [252, 'pass_signal'], [257, 'approach_occ'], [257, 'query']]}, ['set', 'set', 'in-use']), ('control 51', {'release_s': 60, 'events': [[120, 'pass_signal'], [120, 'cancel'], [125, 'approach_clear'], [126, 'cancel'], [136, 'cancel'], [256, 'approach_clear'], [316, 'pass_signal'], [376, 'query'], [377, 'query'], [387, 'cancel'], [387, 'query']]}, ['free', 'free', 'free'])]]
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: query at exactly the release time | ['free'] | ['free'] | Passed |
| regression: re-set at exactly the release time | ['set'] | ['set'] | Passed |
| boundary: second lock after an earlier one | ['locked-until:140'] | ['locked-until:140'] | Passed |
| boundary: train backs out of the approach | ['free'] | ['free'] | Passed |
| boundary: cancel under a train | ['in-use', 'free'] | ['in-use', 'free'] | Passed |
| control 1 | ['free', 'in-use', 'in-use'] | ['free', 'in-use', 'in-use'] | Passed |
| control 4 | ['free', 'free', 'free', 'free', 'free'] | ['free', 'free', 'free', 'free', 'free'] | Passed |
| control 7 | ['free', 'set', 'set'] | ['free', 'set', 'set'] | Passed |
SHA-256 / 6a8402e359b0ea3038c19bfd49f1586a53624890aaf67e6175850c30530ae8d8
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.146828+00:00.
Case digest / 1727450f0bcf8ff9dd3b0571275ad7e848b76645d1e6f70d6ed287e21ba218a9