{"abstract":"A section is released although the train never moved on into the next section.","category":"Railway interlocking logic","checks":8,"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.","contract_signature":"x","evaluation_group":"w2-railway_interlocking_logic-sectional-release","failed_approach":"Requiring a successor for the last section means the route end is never released.","family":"w2-railway_interlocking_logic-sectional-release-successor-occupancy-proof","id":"FA-66941","implementations":{"attempt":{"sha256":"f445f58e6eaf97f87abfc3af81b13390105c83e358d46dd0789e78ba2c9d289d","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(x):\n    route = x['route']\n    seen = set()\n    released = []\n    fault = False\n    occ = set()\n    for sec, ev in x['events']:\n        if sec not in route:\n            continue\n        if ev == 'occ':\n            occ.add(sec)\n            seen.add(sec)\n        else:\n            if sec not in seen:\n                fault = True\n            occ.discard(sec)\n            i = route.index(sec)\n            nxt_ok = route[i + 1] in occ if i < len(route) - 1 else False\n            prev_ok = i == 0 or route[i - 1] in released\n            if not fault and nxt_ok and prev_ok and sec not in released:\n                released.append(sec)\n    return {'released': released, 'fault': fault}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nfixtures = [[('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})]]\nfor label, args, expected in fixtures[N-1]:\n    check(label, solve(args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"b2b62ebd9a0e13692c6f763201a2a2fda054ad6402f21d8c21f057eb2498653c","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(x):\n    route = x['route']\n    seen = set()\n    released = []\n    fault = False\n    occ = set()\n    for sec, ev in x['events']:\n        if sec not in route:\n            continue\n        if ev == 'occ':\n            occ.add(sec)\n            seen.add(sec)\n        else:\n            if sec not in seen:\n                fault = True\n            occ.discard(sec)\n            i = route.index(sec)\n            nxt_ok = i == len(route) - 1 or route[i + 1] in seen\n            prev_ok = i == 0 or route[i - 1] in released\n            if not fault and nxt_ok and prev_ok and sec not in released:\n                released.append(sec)\n    return {'released': released, 'fault': fault}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nfixtures = [[('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})]]\nfor label, args, expected in fixtures[N-1]:\n    check(label, solve(args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"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.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"w2-railway_interlocking_logic-sectional-release-successor-occupancy-proof","generated_at":"2026-09-29T14:47:48.203860+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Interlocking logic decides whether trains may be given authority; a wrong decision at this point either grants unsafe movements or strands traffic.","root_cause":"The successor test uses historical occupancy, so an earlier flicker proves progress.","sha256":"883028d44c77020e3d558f8243401f6f56d5caa98cc6cc65dd662f3c5365aca3","title":"Sectional route release: successor occupancy proof · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verified":true,"visibility":"public","verification":{"attempt":{"elapsed_ms":37.996,"exit_code":1,"observations":[{"actual":{"fault":false,"released":[]},"check":"regression: next section flickered earlier","expected":{"fault":false,"released":[]},"passed":true},{"actual":{"fault":false,"released":["T1","T2"]},"check":"boundary: normal passage","expected":{"fault":false,"released":["T1","T2","T3"]},"passed":false},{"actual":{"fault":false,"released":[]},"check":"sampled regression 63","expected":{"fault":false,"released":[]},"passed":true},{"actual":{"fault":false,"released":[]},"check":"boundary: single section route","expected":{"fault":false,"released":["T1"]},"passed":false},{"actual":{"fault":false,"released":[]},"check":"regression: middle section clears before first","expected":{"fault":false,"released":[]},"passed":true},{"actual":{"fault":false,"released":["T1"]},"check":"control 1","expected":{"fault":false,"released":["T1","T2"]},"passed":false},{"actual":{"fault":false,"released":["T1"]},"check":"control 4","expected":{"fault":false,"released":["T1","T2"]},"passed":false},{"actual":{"fault":true,"released":[]},"check":"control 7","expected":{"fault":true,"released":[]},"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression: next section flickered earlier\", \"actual\": {\"released\": [], \"fault\": false}, \"expected\": {\"released\": [], \"fault\": false}, \"passed\": true}, {\"check\": \"boundary: normal passage\", \"actual\": {\"released\": [\"T1\", \"T2\"], \"fault\": false}, \"expected\": {\"released\": [\"T1\", \"T2\", \"T3\"], \"fault\": false}, \"passed\": false}, {\"check\": \"sampled regression 63\", \"actual\": {\"released\": [], \"fault\": false}, \"expected\": {\"released\": [], \"fault\": false}, \"passed\": true}, {\"check\": \"boundary: single section route\", \"actual\": {\"released\": [], \"fault\": false}, \"expected\": {\"released\": [\"T1\"], \"fault\": false}, \"passed\": false}, {\"check\": \"regression: middle section clears before first\", \"actual\": {\"released\": [], \"fault\": false}, \"expected\": {\"released\": [], \"fault\": false}, \"passed\": true}, {\"check\": \"control 1\", \"actual\": {\"released\": [\"T1\"], \"fault\": false}, \"expected\": {\"released\": [\"T1\", \"T2\"], \"fault\": false}, \"passed\": false}, {\"check\": \"control 4\", \"actual\": {\"released\": [\"T1\"], \"fault\": false}, \"expected\": {\"released\": [\"T1\", \"T2\"], \"fault\": false}, \"passed\": false}, {\"check\": \"control 7\", \"actual\": {\"released\": [], \"fault\": true}, \"expected\": {\"released\": [], \"fault\": true}, \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":38.523,"exit_code":1,"observations":[{"actual":{"fault":false,"released":["T1"]},"check":"regression: next section flickered earlier","expected":{"fault":false,"released":[]},"passed":false},{"actual":{"fault":false,"released":["T1","T2","T3"]},"check":"boundary: normal passage","expected":{"fault":false,"released":["T1","T2","T3"]},"passed":true},{"actual":{"fault":false,"released":["T1"]},"check":"sampled regression 63","expected":{"fault":false,"released":[]},"passed":false},{"actual":{"fault":false,"released":["T1"]},"check":"boundary: single section route","expected":{"fault":false,"released":["T1"]},"passed":true},{"actual":{"fault":false,"released":["T1"]},"check":"regression: middle section clears before first","expected":{"fault":false,"released":[]},"passed":false},{"actual":{"fault":false,"released":["T1","T2"]},"check":"control 1","expected":{"fault":false,"released":["T1","T2"]},"passed":true},{"actual":{"fault":false,"released":["T1","T2"]},"check":"control 4","expected":{"fault":false,"released":["T1","T2"]},"passed":true},{"actual":{"fault":true,"released":[]},"check":"control 7","expected":{"fault":true,"released":[]},"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression: next section flickered earlier\", \"actual\": {\"released\": [\"T1\"], \"fault\": false}, \"expected\": {\"released\": [], \"fault\": false}, \"passed\": false}, {\"check\": \"boundary: normal passage\", \"actual\": {\"released\": [\"T1\", \"T2\", \"T3\"], \"fault\": false}, \"expected\": {\"released\": [\"T1\", \"T2\", \"T3\"], \"fault\": false}, \"passed\": true}, {\"check\": \"sampled regression 63\", \"actual\": {\"released\": [\"T1\"], \"fault\": false}, \"expected\": {\"released\": [], \"fault\": false}, \"passed\": false}, {\"check\": \"boundary: single section route\", \"actual\": {\"released\": [\"T1\"], \"fault\": false}, \"expected\": {\"released\": [\"T1\"], \"fault\": false}, \"passed\": true}, {\"check\": \"regression: middle section clears before first\", \"actual\": {\"released\": [\"T1\"], \"fault\": false}, \"expected\": {\"released\": [], \"fault\": false}, \"passed\": false}, {\"check\": \"control 1\", \"actual\": {\"released\": [\"T1\", \"T2\"], \"fault\": false}, \"expected\": {\"released\": [\"T1\", \"T2\"], \"fault\": false}, \"passed\": true}, {\"check\": \"control 4\", \"actual\": {\"released\": [\"T1\", \"T2\"], \"fault\": false}, \"expected\": {\"released\": [\"T1\", \"T2\"], \"fault\": false}, \"passed\": true}, {\"check\": \"control 7\", \"actual\": {\"released\": [], \"fault\": true}, \"expected\": {\"released\": [], \"fault\": true}, \"passed\": true}], \"passed\": false}\n"}},"member_only":{"stages":["fixed"],"fields":["implementations.fixed","verification.fixed","harness","repair"],"note":"The verified repair, its recorded checks, the repair description, and the scoring harness are available to members."}}