FA-66866 / Railway interlocking logic / Open access

Four-aspect signal chain evaluation: dark signal treatment · case 01

The signal in rear of a dark signal shows a proceed aspect.

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

ROOT CAUSE

A DARK signal ahead is treated like a red one, so the rear signal offers a caution instead of being held at danger.

VERIFIED REPAIR

Hold the rear signal at R whenever the next signal is DARK.

Unsuccessful approach: Holding at R only on open lines still lets a caution approach a dark signal near a buffer stop.

Case contract

Signals 0..n-1 each protect one block; occupied[i] is the block after signal i. Evaluate from the far end: a signal shows R if its block is occupied, else Y if the next signal is R, R if the next signal is DARK, YY if the next is Y, otherwise G. Beyond the last signal the next aspect is G on an open line and R at a buffer stop. A diverging signal is capped at Y. A signal whose red lamp has failed shows DARK instead of R.

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):
    occ = x['occupied']
    n = len(occ)
    fail = set(x['lamp_fail'])
    div = set(x['diverging'])
    nxt = 'G' if x['open_end'] else 'R'
    out = [None] * n
    for i in range(n - 1, -1, -1):
        if occ[i]:
            a = 'R'
        elif nxt in ('R', 'DARK'):
            a = 'Y'
        elif nxt == 'Y':
            a = 'YY'
        else:
            a = 'G'
        if i in div and a in ('YY', 'G'):
            a = 'Y'
        if a == 'R' and i in fail:
            a = 'DARK'
        out[i] = a
        nxt = a
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 56', {'occupied': [False, False, False, True, False], 'lamp_fail': [3], 'diverging': [], 'open_end': False}, ['YY', 'Y', 'R', 'DARK', 'Y']), ('sampled regression 63', {'occupied': [False, False, False, False, False, True, False], 'lamp_fail': [5, 6], 'diverging': [], 'open_end': True}, ['G', 'G', 'YY', 'Y', 'R', 'DARK', 'G']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: failed red lamp on a clear signal', {'occupied': [False, False, False], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['G', 'G', 'G']), ('control 1', {'occupied': [False, True, False, False, False, False], 'lamp_fail': [0], 'diverging': [], 'open_end': False}, ['Y', 'R', 'G', 'G', 'YY', 'Y']), ('control 4', {'occupied': [False, True], 'lamp_fail': [], 'diverging': [], 'open_end': False}, ['Y', 'R']), ('control 7', {'occupied': [True, False, False, True], 'lamp_fail': [], 'diverging': [3], 'open_end': True}, ['R', 'YY', 'Y', 'R'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('sampled regression 56', {'occupied': [False, False, False, True, False], 'lamp_fail': [3], 'diverging': [], 'open_end': False}, ['YY', 'Y', 'R', 'DARK', 'Y']), ('boundary: diverging junction behind a double yellow', {'occupied': [False, False, True], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['Y', 'Y', 'R']), ('boundary: diverging junction behind a green', {'occupied': [False, False, False], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['Y', 'G', 'G']), ('control 12', {'occupied': [False, False], 'lamp_fail': [0], 'diverging': [], 'open_end': False}, ['YY', 'Y']), ('control 15', {'occupied': [False, True], 'lamp_fail': [], 'diverging': [], 'open_end': True}, ['Y', 'R']), ('control 18', {'occupied': [False, False], 'lamp_fail': [], 'diverging': [], 'open_end': True}, ['G', 'G'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 76', {'occupied': [False, True, False, True, True], 'lamp_fail': [3, 4], 'diverging': [1], 'open_end': False}, ['Y', 'R', 'R', 'DARK', 'DARK']), ('sampled regression 45', {'occupied': [True, False, False, True], 'lamp_fail': [3], 'diverging': [1], 'open_end': True}, ['R', 'Y', 'R', 'DARK']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: buffer stop at the end', {'occupied': [False, False, False], 'lamp_fail': [], 'diverging': [], 'open_end': False}, ['G', 'YY', 'Y']), ('control 23', {'occupied': [True, False, True], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['R', 'Y', 'R']), ('control 26', {'occupied': [False, False, False, True], 'lamp_fail': [], 'diverging': [3], 'open_end': False}, ['G', 'YY', 'Y', 'R']), ('control 29', {'occupied': [False, True], 'lamp_fail': [], 'diverging': [], 'open_end': False}, ['Y', 'R'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 78', {'occupied': [False, False, False, False, True, False, False], 'lamp_fail': [4, 5], 'diverging': [6], 'open_end': False}, ['G', 'YY', 'Y', 'R', 'DARK', 'YY', 'Y']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: train two blocks ahead', {'occupied': [False, False, True, False], 'lamp_fail': [], 'diverging': [], 'open_end': True}, ['YY', 'Y', 'R', 'G']), ('boundary: dark signal at the buffer end', {'occupied': [False, False], 'lamp_fail': [1], 'diverging': [], 'open_end': False}, ['YY', 'Y']), ('control 34', {'occupied': [False, False, False, False, False, False, False], 'lamp_fail': [], 'diverging': [1], 'open_end': False}, ['YY', 'Y', 'G', 'G', 'G', 'YY', 'Y']), ('control 37', {'occupied': [False, False, False, False], 'lamp_fail': [0], 'diverging': [0, 3], 'open_end': True}, ['Y', 'G', 'YY', 'Y']), ('control 40', {'occupied': [False, False, False, False], 'lamp_fail': [0], 'diverging': [0], 'open_end': True}, ['Y', 'G', 'G', 'G'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 80', {'occupied': [False, False, False, False, False, False, True], 'lamp_fail': [6], 'diverging': [], 'open_end': False}, ['G', 'G', 'G', 'YY', 'Y', 'R', 'DARK']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: failed red lamp on a clear signal', {'occupied': [False, False, False], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['G', 'G', 'G']), ('boundary: diverging junction behind a double yellow', {'occupied': [False, False, True], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['Y', 'Y', 'R']), ('sampled regression 45', {'occupied': [True, False, False, True], 'lamp_fail': [3], 'diverging': [1], 'open_end': True}, ['R', 'Y', 'R', 'DARK']), ('control 48', {'occupied': [False, False, False, False], 'lamp_fail': [1], 'diverging': [2], 'open_end': True}, ['G', 'YY', 'Y', 'G']), ('control 51', {'occupied': [False, False, False, True], 'lamp_fail': [], 'diverging': [0, 2, 3], 'open_end': True}, ['Y', 'YY', 'Y', 'R'])]]
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: dark signal ahead	`['Y', 'DARK']`	`['R', 'DARK']`	Failed
sampled regression 56	`['G', 'YY', 'Y', 'DARK', 'Y']`	`['YY', 'Y', 'R', 'DARK', 'Y']`	Failed
sampled regression 63	`['G', 'G', 'G', 'YY', 'Y', 'DARK', 'G']`	`['G', 'G', 'YY', 'Y', 'R', 'DARK', 'G']`	Failed
sampled regression 75	`['Y', 'Y', 'DARK', 'Y']`	`['Y', 'R', 'DARK', 'Y']`	Failed
boundary: failed red lamp on a clear signal	`['G', 'G', 'G']`	`['G', 'G', 'G']`	Passed
control 1	`['Y', 'R', 'G', 'G', 'YY', 'Y']`	`['Y', 'R', 'G', 'G', 'YY', 'Y']`	Passed
control 4	`['Y', 'R']`	`['Y', 'R']`	Passed
control 7	`['R', 'YY', 'Y', 'R']`	`['R', 'YY', 'Y', 'R']`	Passed

SHA-256 / 32fa7600a402baee8f9393633c8f85c02f08eba7a5eac9e8676dde8421481ebc

2 / The unsuccessful fix

Exit 1

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

N = 1
observations = []
def solve(x):
    occ = x['occupied']
    n = len(occ)
    fail = set(x['lamp_fail'])
    div = set(x['diverging'])
    nxt = 'G' if x['open_end'] else 'R'
    out = [None] * n
    for i in range(n - 1, -1, -1):
        if occ[i]:
            a = 'R'
        elif nxt in ('R', 'DARK'):
            a = 'R' if nxt == 'DARK' and x['open_end'] else 'Y'
        elif nxt == 'Y':
            a = 'YY'
        else:
            a = 'G'
        if i in div and a in ('YY', 'G'):
            a = 'Y'
        if a == 'R' and i in fail:
            a = 'DARK'
        out[i] = a
        nxt = a
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 56', {'occupied': [False, False, False, True, False], 'lamp_fail': [3], 'diverging': [], 'open_end': False}, ['YY', 'Y', 'R', 'DARK', 'Y']), ('sampled regression 63', {'occupied': [False, False, False, False, False, True, False], 'lamp_fail': [5, 6], 'diverging': [], 'open_end': True}, ['G', 'G', 'YY', 'Y', 'R', 'DARK', 'G']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: failed red lamp on a clear signal', {'occupied': [False, False, False], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['G', 'G', 'G']), ('control 1', {'occupied': [False, True, False, False, False, False], 'lamp_fail': [0], 'diverging': [], 'open_end': False}, ['Y', 'R', 'G', 'G', 'YY', 'Y']), ('control 4', {'occupied': [False, True], 'lamp_fail': [], 'diverging': [], 'open_end': False}, ['Y', 'R']), ('control 7', {'occupied': [True, False, False, True], 'lamp_fail': [], 'diverging': [3], 'open_end': True}, ['R', 'YY', 'Y', 'R'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('sampled regression 56', {'occupied': [False, False, False, True, False], 'lamp_fail': [3], 'diverging': [], 'open_end': False}, ['YY', 'Y', 'R', 'DARK', 'Y']), ('boundary: diverging junction behind a double yellow', {'occupied': [False, False, True], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['Y', 'Y', 'R']), ('boundary: diverging junction behind a green', {'occupied': [False, False, False], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['Y', 'G', 'G']), ('control 12', {'occupied': [False, False], 'lamp_fail': [0], 'diverging': [], 'open_end': False}, ['YY', 'Y']), ('control 15', {'occupied': [False, True], 'lamp_fail': [], 'diverging': [], 'open_end': True}, ['Y', 'R']), ('control 18', {'occupied': [False, False], 'lamp_fail': [], 'diverging': [], 'open_end': True}, ['G', 'G'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 76', {'occupied': [False, True, False, True, True], 'lamp_fail': [3, 4], 'diverging': [1], 'open_end': False}, ['Y', 'R', 'R', 'DARK', 'DARK']), ('sampled regression 45', {'occupied': [True, False, False, True], 'lamp_fail': [3], 'diverging': [1], 'open_end': True}, ['R', 'Y', 'R', 'DARK']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: buffer stop at the end', {'occupied': [False, False, False], 'lamp_fail': [], 'diverging': [], 'open_end': False}, ['G', 'YY', 'Y']), ('control 23', {'occupied': [True, False, True], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['R', 'Y', 'R']), ('control 26', {'occupied': [False, False, False, True], 'lamp_fail': [], 'diverging': [3], 'open_end': False}, ['G', 'YY', 'Y', 'R']), ('control 29', {'occupied': [False, True], 'lamp_fail': [], 'diverging': [], 'open_end': False}, ['Y', 'R'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 78', {'occupied': [False, False, False, False, True, False, False], 'lamp_fail': [4, 5], 'diverging': [6], 'open_end': False}, ['G', 'YY', 'Y', 'R', 'DARK', 'YY', 'Y']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: train two blocks ahead', {'occupied': [False, False, True, False], 'lamp_fail': [], 'diverging': [], 'open_end': True}, ['YY', 'Y', 'R', 'G']), ('boundary: dark signal at the buffer end', {'occupied': [False, False], 'lamp_fail': [1], 'diverging': [], 'open_end': False}, ['YY', 'Y']), ('control 34', {'occupied': [False, False, False, False, False, False, False], 'lamp_fail': [], 'diverging': [1], 'open_end': False}, ['YY', 'Y', 'G', 'G', 'G', 'YY', 'Y']), ('control 37', {'occupied': [False, False, False, False], 'lamp_fail': [0], 'diverging': [0, 3], 'open_end': True}, ['Y', 'G', 'YY', 'Y']), ('control 40', {'occupied': [False, False, False, False], 'lamp_fail': [0], 'diverging': [0], 'open_end': True}, ['Y', 'G', 'G', 'G'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 80', {'occupied': [False, False, False, False, False, False, True], 'lamp_fail': [6], 'diverging': [], 'open_end': False}, ['G', 'G', 'G', 'YY', 'Y', 'R', 'DARK']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: failed red lamp on a clear signal', {'occupied': [False, False, False], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['G', 'G', 'G']), ('boundary: diverging junction behind a double yellow', {'occupied': [False, False, True], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['Y', 'Y', 'R']), ('sampled regression 45', {'occupied': [True, False, False, True], 'lamp_fail': [3], 'diverging': [1], 'open_end': True}, ['R', 'Y', 'R', 'DARK']), ('control 48', {'occupied': [False, False, False, False], 'lamp_fail': [1], 'diverging': [2], 'open_end': True}, ['G', 'YY', 'Y', 'G']), ('control 51', {'occupied': [False, False, False, True], 'lamp_fail': [], 'diverging': [0, 2, 3], 'open_end': True}, ['Y', 'YY', 'Y', 'R'])]]
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: dark signal ahead	`['R', 'DARK']`	`['R', 'DARK']`	Passed
sampled regression 56	`['G', 'YY', 'Y', 'DARK', 'Y']`	`['YY', 'Y', 'R', 'DARK', 'Y']`	Failed
sampled regression 63	`['G', 'G', 'YY', 'Y', 'R', 'DARK', 'G']`	`['G', 'G', 'YY', 'Y', 'R', 'DARK', 'G']`	Passed
sampled regression 75	`['Y', 'Y', 'DARK', 'Y']`	`['Y', 'R', 'DARK', 'Y']`	Failed
boundary: failed red lamp on a clear signal	`['G', 'G', 'G']`	`['G', 'G', 'G']`	Passed
control 1	`['Y', 'R', 'G', 'G', 'YY', 'Y']`	`['Y', 'R', 'G', 'G', 'YY', 'Y']`	Passed
control 4	`['Y', 'R']`	`['Y', 'R']`	Passed
control 7	`['R', 'YY', 'Y', 'R']`	`['R', 'YY', 'Y', 'R']`	Passed

SHA-256 / aa673f35d15a2931920c3d310dd5f3979272e0b728f69aed270db7bbf6038fbb

3 / The verified repair

Exit 0

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

N = 1
observations = []
def solve(x):
    occ = x['occupied']
    n = len(occ)
    fail = set(x['lamp_fail'])
    div = set(x['diverging'])
    nxt = 'G' if x['open_end'] else 'R'
    out = [None] * n
    for i in range(n - 1, -1, -1):
        if occ[i]:
            a = 'R'
        elif nxt in ('R', 'DARK'):
            a = 'R' if nxt == 'DARK' else 'Y'
        elif nxt == 'Y':
            a = 'YY'
        else:
            a = 'G'
        if i in div and a in ('YY', 'G'):
            a = 'Y'
        if a == 'R' and i in fail:
            a = 'DARK'
        out[i] = a
        nxt = a
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 56', {'occupied': [False, False, False, True, False], 'lamp_fail': [3], 'diverging': [], 'open_end': False}, ['YY', 'Y', 'R', 'DARK', 'Y']), ('sampled regression 63', {'occupied': [False, False, False, False, False, True, False], 'lamp_fail': [5, 6], 'diverging': [], 'open_end': True}, ['G', 'G', 'YY', 'Y', 'R', 'DARK', 'G']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: failed red lamp on a clear signal', {'occupied': [False, False, False], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['G', 'G', 'G']), ('control 1', {'occupied': [False, True, False, False, False, False], 'lamp_fail': [0], 'diverging': [], 'open_end': False}, ['Y', 'R', 'G', 'G', 'YY', 'Y']), ('control 4', {'occupied': [False, True], 'lamp_fail': [], 'diverging': [], 'open_end': False}, ['Y', 'R']), ('control 7', {'occupied': [True, False, False, True], 'lamp_fail': [], 'diverging': [3], 'open_end': True}, ['R', 'YY', 'Y', 'R'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('sampled regression 56', {'occupied': [False, False, False, True, False], 'lamp_fail': [3], 'diverging': [], 'open_end': False}, ['YY', 'Y', 'R', 'DARK', 'Y']), ('boundary: diverging junction behind a double yellow', {'occupied': [False, False, True], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['Y', 'Y', 'R']), ('boundary: diverging junction behind a green', {'occupied': [False, False, False], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['Y', 'G', 'G']), ('control 12', {'occupied': [False, False], 'lamp_fail': [0], 'diverging': [], 'open_end': False}, ['YY', 'Y']), ('control 15', {'occupied': [False, True], 'lamp_fail': [], 'diverging': [], 'open_end': True}, ['Y', 'R']), ('control 18', {'occupied': [False, False], 'lamp_fail': [], 'diverging': [], 'open_end': True}, ['G', 'G'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 76', {'occupied': [False, True, False, True, True], 'lamp_fail': [3, 4], 'diverging': [1], 'open_end': False}, ['Y', 'R', 'R', 'DARK', 'DARK']), ('sampled regression 45', {'occupied': [True, False, False, True], 'lamp_fail': [3], 'diverging': [1], 'open_end': True}, ['R', 'Y', 'R', 'DARK']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: buffer stop at the end', {'occupied': [False, False, False], 'lamp_fail': [], 'diverging': [], 'open_end': False}, ['G', 'YY', 'Y']), ('control 23', {'occupied': [True, False, True], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['R', 'Y', 'R']), ('control 26', {'occupied': [False, False, False, True], 'lamp_fail': [], 'diverging': [3], 'open_end': False}, ['G', 'YY', 'Y', 'R']), ('control 29', {'occupied': [False, True], 'lamp_fail': [], 'diverging': [], 'open_end': False}, ['Y', 'R'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 78', {'occupied': [False, False, False, False, True, False, False], 'lamp_fail': [4, 5], 'diverging': [6], 'open_end': False}, ['G', 'YY', 'Y', 'R', 'DARK', 'YY', 'Y']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: train two blocks ahead', {'occupied': [False, False, True, False], 'lamp_fail': [], 'diverging': [], 'open_end': True}, ['YY', 'Y', 'R', 'G']), ('boundary: dark signal at the buffer end', {'occupied': [False, False], 'lamp_fail': [1], 'diverging': [], 'open_end': False}, ['YY', 'Y']), ('control 34', {'occupied': [False, False, False, False, False, False, False], 'lamp_fail': [], 'diverging': [1], 'open_end': False}, ['YY', 'Y', 'G', 'G', 'G', 'YY', 'Y']), ('control 37', {'occupied': [False, False, False, False], 'lamp_fail': [0], 'diverging': [0, 3], 'open_end': True}, ['Y', 'G', 'YY', 'Y']), ('control 40', {'occupied': [False, False, False, False], 'lamp_fail': [0], 'diverging': [0], 'open_end': True}, ['Y', 'G', 'G', 'G'])], [('regression: dark signal ahead', {'occupied': [False, True], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['R', 'DARK']), ('sampled regression 80', {'occupied': [False, False, False, False, False, False, True], 'lamp_fail': [6], 'diverging': [], 'open_end': False}, ['G', 'G', 'G', 'YY', 'Y', 'R', 'DARK']), ('sampled regression 75', {'occupied': [False, False, True, False], 'lamp_fail': [0, 2], 'diverging': [0, 2, 3], 'open_end': False}, ['Y', 'R', 'DARK', 'Y']), ('boundary: failed red lamp on a clear signal', {'occupied': [False, False, False], 'lamp_fail': [1], 'diverging': [], 'open_end': True}, ['G', 'G', 'G']), ('boundary: diverging junction behind a double yellow', {'occupied': [False, False, True], 'lamp_fail': [], 'diverging': [0], 'open_end': True}, ['Y', 'Y', 'R']), ('sampled regression 45', {'occupied': [True, False, False, True], 'lamp_fail': [3], 'diverging': [1], 'open_end': True}, ['R', 'Y', 'R', 'DARK']), ('control 48', {'occupied': [False, False, False, False], 'lamp_fail': [1], 'diverging': [2], 'open_end': True}, ['G', 'YY', 'Y', 'G']), ('control 51', {'occupied': [False, False, False, True], 'lamp_fail': [], 'diverging': [0, 2, 3], 'open_end': True}, ['Y', 'YY', 'Y', 'R'])]]
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: dark signal ahead	`['R', 'DARK']`	`['R', 'DARK']`	Passed
sampled regression 56	`['YY', 'Y', 'R', 'DARK', 'Y']`	`['YY', 'Y', 'R', 'DARK', 'Y']`	Passed
sampled regression 63	`['G', 'G', 'YY', 'Y', 'R', 'DARK', 'G']`	`['G', 'G', 'YY', 'Y', 'R', 'DARK', 'G']`	Passed
sampled regression 75	`['Y', 'R', 'DARK', 'Y']`	`['Y', 'R', 'DARK', 'Y']`	Passed
boundary: failed red lamp on a clear signal	`['G', 'G', 'G']`	`['G', 'G', 'G']`	Passed
control 1	`['Y', 'R', 'G', 'G', 'YY', 'Y']`	`['Y', 'R', 'G', 'G', 'YY', 'Y']`	Passed
control 4	`['Y', 'R']`	`['Y', 'R']`	Passed
control 7	`['R', 'YY', 'Y', 'R']`	`['R', 'YY', 'Y', 'R']`	Passed

SHA-256 / 9c9fe436d5f63edcfe21965df96ad104dacbb65451823b5a221d3bfd9e12d6b0

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

Case digest / c0d214e2fe0da81c038b0dbc5a99fee8beb7bc4c34fe49ec16359577632c9e9d