FA-66941 / Railway interlocking logic / Open access

Sectional route release: successor occupancy proof · case 01

A section is released although the train never moved on into the next section.

Verified by executionVariant 1 · 8 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

The successor test uses historical occupancy, so an earlier flicker proves progress.

VERIFIED REPAIR

Require the next route section to be occupied at the moment the section clears; the last section needs no successor.

Unsuccessful approach: Requiring a successor for the last section means the route end is never released.

Case contract

Sections of a locked route are released in route order as the train passes. A section is released when it clears, it was seen occupied earlier, its predecessor is already released (or it is the first), and the next route section is currently occupied (or it is the last). A clear of a never-occupied route section latches a fault that stops all further release. Events for sections outside the route are ignored. Output released sections in release order and the fault flag.

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):
    route = x['route']
    seen = set()
    released = []
    fault = False
    occ = set()
    for sec, ev in x['events']:
        if sec not in route:
            continue
        if ev == 'occ':
            occ.add(sec)
            seen.add(sec)
        else:
            if sec not in seen:
                fault = True
            occ.discard(sec)
            i = route.index(sec)
            nxt_ok = i == len(route) - 1 or route[i + 1] in seen
            prev_ok = i == 0 or route[i - 1] in released
            if not fault and nxt_ok and prev_ok and sec not in released:
                released.append(sec)
    return {'released': released, 'fault': fault}
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: normal passage', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('sampled regression 63', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 1', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['Z9', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 4', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 7', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'clr'], ['Z9', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': [], 'fault': True})], [('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 4', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('boundary: phantom clear then passage', {'route': ['T1', 'T2'], 'events': [['T2', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': [], 'fault': True}), ('control 12', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T3', 'occ'], ['T1', 'occ'], ['T1', 'clr'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('control 15', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T4', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1', 'T2', 'T3', 'T4'], 'fault': False}), ('control 18', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T1', 'occ'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False})], [('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: foreign section noise', {'route': ['T1', 'T2'], 'events': [['Z9', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('sampled regression 25', {'route': ['T1', 'T2', 'T3', 'T4', 'T5'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T5', 'occ'], ['T4', 'clr'], ['T5', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 12', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T3', 'occ'], ['T1', 'occ'], ['T1', 'clr'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('boundary: phantom clear on first section', {'route': ['T1', 'T2'], 'events': [['T1', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': True}), ('control 23', {'route': ['T1', 'T2', 'T3'], 'events': [['T3', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['Z9', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': [], 'fault': True}), ('control 26', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T1', 'clr'], ['T4', 'clr'], ['T4', 'occ']]}, {'released': ['T1', 'T2', 'T3', 'T4'], 'fault': False}), ('control 29', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False})], [('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: normal passage', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('sampled regression 79', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['Z9', 'clr'], ['T2', 'clr'], ['T4', 'occ'], ['T4', 'clr'], ['T3', 'clr'], ['T3', 'clr'], ['T4', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 18', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T1', 'occ'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('control 34', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'occ'], ['Z9', 'clr'], ['T1', 'clr'], ['T2', 'clr'], ['Z9', 'occ']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 37', {'route': ['T1', 'T2', 'T3', 'T4', 'T5'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T5', 'occ'], ['T4', 'clr'], ['T5', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1', 'T2', 'T3', 'T4', 'T5'], 'fault': False}), ('control 40', {'route': ['T1', 'T2'], 'events': [['T2', 'occ'], ['T1', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['T2', 'occ'], ['T2', 'clr']]}, {'released': [], 'fault': False})], [('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 29', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('boundary: normal passage', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('control 45', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T3', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['Z9', 'occ'], ['T3', 'clr'], ['T4', 'clr']]}, {'released': ['T1', 'T2', 'T3', 'T4'], 'fault': False}), ('control 48', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['Z9', 'occ'], ['T2', 'clr'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': True}), ('control 51', {'route': ['T1', 'T2', 'T3'], 'events': [['Z9', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T2', 'occ'], ['T3', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False})]]
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: next section flickered earlier	`{'fault': False, 'released': ['T1']}`	`{'fault': False, 'released': []}`	Failed
boundary: normal passage	`{'fault': False, 'released': ['T1', 'T2', 'T3']}`	`{'fault': False, 'released': ['T1', 'T2', 'T3']}`	Passed
sampled regression 63	`{'fault': False, 'released': ['T1']}`	`{'fault': False, 'released': []}`	Failed
boundary: single section route	`{'fault': False, 'released': ['T1']}`	`{'fault': False, 'released': ['T1']}`	Passed
regression: middle section clears before first	`{'fault': False, 'released': ['T1']}`	`{'fault': False, 'released': []}`	Failed
control 1	`{'fault': False, 'released': ['T1', 'T2']}`	`{'fault': False, 'released': ['T1', 'T2']}`	Passed
control 4	`{'fault': False, 'released': ['T1', 'T2']}`	`{'fault': False, 'released': ['T1', 'T2']}`	Passed
control 7	`{'fault': True, 'released': []}`	`{'fault': True, 'released': []}`	Passed

SHA-256 / b2b62ebd9a0e13692c6f763201a2a2fda054ad6402f21d8c21f057eb2498653c

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(x):
    route = x['route']
    seen = set()
    released = []
    fault = False
    occ = set()
    for sec, ev in x['events']:
        if sec not in route:
            continue
        if ev == 'occ':
            occ.add(sec)
            seen.add(sec)
        else:
            if sec not in seen:
                fault = True
            occ.discard(sec)
            i = route.index(sec)
            nxt_ok = route[i + 1] in occ if i < len(route) - 1 else False
            prev_ok = i == 0 or route[i - 1] in released
            if not fault and nxt_ok and prev_ok and sec not in released:
                released.append(sec)
    return {'released': released, 'fault': fault}
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: normal passage', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('sampled regression 63', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 1', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['Z9', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 4', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 7', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'clr'], ['Z9', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': [], 'fault': True})], [('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 4', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('boundary: phantom clear then passage', {'route': ['T1', 'T2'], 'events': [['T2', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': [], 'fault': True}), ('control 12', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T3', 'occ'], ['T1', 'occ'], ['T1', 'clr'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('control 15', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T4', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1', 'T2', 'T3', 'T4'], 'fault': False}), ('control 18', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T1', 'occ'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False})], [('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: foreign section noise', {'route': ['T1', 'T2'], 'events': [['Z9', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('sampled regression 25', {'route': ['T1', 'T2', 'T3', 'T4', 'T5'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T5', 'occ'], ['T4', 'clr'], ['T5', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 12', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T3', 'occ'], ['T1', 'occ'], ['T1', 'clr'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('boundary: phantom clear on first section', {'route': ['T1', 'T2'], 'events': [['T1', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': True}), ('control 23', {'route': ['T1', 'T2', 'T3'], 'events': [['T3', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['Z9', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': [], 'fault': True}), ('control 26', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T1', 'clr'], ['T4', 'clr'], ['T4', 'occ']]}, {'released': ['T1', 'T2', 'T3', 'T4'], 'fault': False}), ('control 29', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False})], [('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: normal passage', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('sampled regression 79', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['Z9', 'clr'], ['T2', 'clr'], ['T4', 'occ'], ['T4', 'clr'], ['T3', 'clr'], ['T3', 'clr'], ['T4', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 18', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T1', 'occ'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('control 34', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'occ'], ['Z9', 'clr'], ['T1', 'clr'], ['T2', 'clr'], ['Z9', 'occ']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 37', {'route': ['T1', 'T2', 'T3', 'T4', 'T5'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T5', 'occ'], ['T4', 'clr'], ['T5', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1', 'T2', 'T3', 'T4', 'T5'], 'fault': False}), ('control 40', {'route': ['T1', 'T2'], 'events': [['T2', 'occ'], ['T1', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['T2', 'occ'], ['T2', 'clr']]}, {'released': [], 'fault': False})], [('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 29', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('boundary: normal passage', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('control 45', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T3', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['Z9', 'occ'], ['T3', 'clr'], ['T4', 'clr']]}, {'released': ['T1', 'T2', 'T3', 'T4'], 'fault': False}), ('control 48', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['Z9', 'occ'], ['T2', 'clr'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': True}), ('control 51', {'route': ['T1', 'T2', 'T3'], 'events': [['Z9', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T2', 'occ'], ['T3', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False})]]
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: next section flickered earlier	`{'fault': False, 'released': []}`	`{'fault': False, 'released': []}`	Passed
boundary: normal passage	`{'fault': False, 'released': ['T1', 'T2']}`	`{'fault': False, 'released': ['T1', 'T2', 'T3']}`	Failed
sampled regression 63	`{'fault': False, 'released': []}`	`{'fault': False, 'released': []}`	Passed
boundary: single section route	`{'fault': False, 'released': []}`	`{'fault': False, 'released': ['T1']}`	Failed
regression: middle section clears before first	`{'fault': False, 'released': []}`	`{'fault': False, 'released': []}`	Passed
control 1	`{'fault': False, 'released': ['T1']}`	`{'fault': False, 'released': ['T1', 'T2']}`	Failed
control 4	`{'fault': False, 'released': ['T1']}`	`{'fault': False, 'released': ['T1', 'T2']}`	Failed
control 7	`{'fault': True, 'released': []}`	`{'fault': True, 'released': []}`	Passed

SHA-256 / f445f58e6eaf97f87abfc3af81b13390105c83e358d46dd0789e78ba2c9d289d

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(x):
    route = x['route']
    seen = set()
    released = []
    fault = False
    occ = set()
    for sec, ev in x['events']:
        if sec not in route:
            continue
        if ev == 'occ':
            occ.add(sec)
            seen.add(sec)
        else:
            if sec not in seen:
                fault = True
            occ.discard(sec)
            i = route.index(sec)
            nxt_ok = i == len(route) - 1 or route[i + 1] in occ
            prev_ok = i == 0 or route[i - 1] in released
            if not fault and nxt_ok and prev_ok and sec not in released:
                released.append(sec)
    return {'released': released, 'fault': fault}
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: normal passage', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('sampled regression 63', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 1', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['Z9', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 4', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 7', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'clr'], ['Z9', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': [], 'fault': True})], [('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 4', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('boundary: phantom clear then passage', {'route': ['T1', 'T2'], 'events': [['T2', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': [], 'fault': True}), ('control 12', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T3', 'occ'], ['T1', 'occ'], ['T1', 'clr'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('control 15', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T4', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1', 'T2', 'T3', 'T4'], 'fault': False}), ('control 18', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T1', 'occ'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False})], [('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: foreign section noise', {'route': ['T1', 'T2'], 'events': [['Z9', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('sampled regression 25', {'route': ['T1', 'T2', 'T3', 'T4', 'T5'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T5', 'occ'], ['T4', 'clr'], ['T5', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 12', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T3', 'occ'], ['T1', 'occ'], ['T1', 'clr'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('boundary: phantom clear on first section', {'route': ['T1', 'T2'], 'events': [['T1', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': True}), ('control 23', {'route': ['T1', 'T2', 'T3'], 'events': [['T3', 'clr'], ['T1', 'occ'], ['T2', 'occ'], ['Z9', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': [], 'fault': True}), ('control 26', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T1', 'clr'], ['T4', 'clr'], ['T4', 'occ']]}, {'released': ['T1', 'T2', 'T3', 'T4'], 'fault': False}), ('control 29', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False})], [('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: normal passage', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('sampled regression 79', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['Z9', 'clr'], ['T2', 'clr'], ['T4', 'occ'], ['T4', 'clr'], ['T3', 'clr'], ['T3', 'clr'], ['T4', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 18', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T1', 'occ'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('control 34', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'occ'], ['Z9', 'clr'], ['T1', 'clr'], ['T2', 'clr'], ['Z9', 'occ']]}, {'released': ['T1', 'T2'], 'fault': False}), ('control 37', {'route': ['T1', 'T2', 'T3', 'T4', 'T5'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['T3', 'clr'], ['T5', 'occ'], ['T4', 'clr'], ['T5', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1', 'T2', 'T3', 'T4', 'T5'], 'fault': False}), ('control 40', {'route': ['T1', 'T2'], 'events': [['T2', 'occ'], ['T1', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['T2', 'occ'], ['T2', 'clr']]}, {'released': [], 'fault': False})], [('regression: next section flickered earlier', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('boundary: single section route', {'route': ['T1'], 'events': [['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1'], 'fault': False}), ('regression: middle section clears before first', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T1', 'clr']]}, {'released': [], 'fault': False}), ('control 29', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr']]}, {'released': ['T1', 'T2'], 'fault': False}), ('boundary: normal passage', {'route': ['T1', 'T2', 'T3'], 'events': [['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T3', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False}), ('control 45', {'route': ['T1', 'T2', 'T3', 'T4'], 'events': [['T1', 'occ'], ['T3', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T1', 'clr'], ['T3', 'occ'], ['T2', 'clr'], ['T4', 'occ'], ['Z9', 'occ'], ['T3', 'clr'], ['T4', 'clr']]}, {'released': ['T1', 'T2', 'T3', 'T4'], 'fault': False}), ('control 48', {'route': ['T1', 'T2'], 'events': [['T1', 'occ'], ['Z9', 'occ'], ['T2', 'clr'], ['T2', 'occ'], ['T1', 'clr'], ['T2', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': [], 'fault': True}), ('control 51', {'route': ['T1', 'T2', 'T3'], 'events': [['Z9', 'occ'], ['T1', 'occ'], ['T2', 'occ'], ['T1', 'clr'], ['T3', 'occ'], ['T3', 'occ'], ['T2', 'clr'], ['T2', 'occ'], ['T3', 'clr'], ['T1', 'occ'], ['T1', 'clr']]}, {'released': ['T1', 'T2', 'T3'], 'fault': False})]]
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: next section flickered earlier	`{'fault': False, 'released': []}`	`{'fault': False, 'released': []}`	Passed
boundary: normal passage	`{'fault': False, 'released': ['T1', 'T2', 'T3']}`	`{'fault': False, 'released': ['T1', 'T2', 'T3']}`	Passed
sampled regression 63	`{'fault': False, 'released': []}`	`{'fault': False, 'released': []}`	Passed
boundary: single section route	`{'fault': False, 'released': ['T1']}`	`{'fault': False, 'released': ['T1']}`	Passed
regression: middle section clears before first	`{'fault': False, 'released': []}`	`{'fault': False, 'released': []}`	Passed
control 1	`{'fault': False, 'released': ['T1', 'T2']}`	`{'fault': False, 'released': ['T1', 'T2']}`	Passed
control 4	`{'fault': False, 'released': ['T1', 'T2']}`	`{'fault': False, 'released': ['T1', 'T2']}`	Passed
control 7	`{'fault': True, 'released': []}`	`{'fault': True, 'released': []}`	Passed

SHA-256 / 893c99aff3439c814f9a5a05d37006c1e54ab578cac8feb796e4cc7655a30ee7

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.203860+00:00.

Case digest / 1fb8563616761327aa3dc86012a52d1f28ec0ebf607d1945a34c3a61b59d86a9