Signal Box — the domain

We're going to use as an example a common, real-world, life-or-death situation: train switching systems.

Our world is a passing loop on a single-track railway — the arrangement that lets two trains travelling in opposite directions get past each other. This is what it looks like when everything is working:

The passing move: T1 enters the loop from the west while T2 takes the main from the east. Both signals are lawfully green.

A and E are the single-track approaches, west and east. L is the loop (eastbound traffic), M is the main (westbound).
P1 and P2 are the points (switches) at each end of the loop. Each is set either toward the loop or toward the main; the heavy black blade in the diagram shows the current setting.
SA, SL, SE, SM are the signals, one per permitted move: SA admits a train from A into the loop, SL releases it east, SE admits a train from E onto the main, SM releases it west. Green means go.
T1 and T2 are the trains. A train sits on exactly one segment, or is off-scene.

These are the failure states a real interlocking exists to prevent:

collision — two trains on one segment

conflicting greens — two signals clear clashing routes at once

derailment — a signal clears a train onto points set against it

There's a fourth family, green into occupied track (a signal clearing a train toward a segment that already has one on it), and a zeroth: states so malformed they don't describe a railway at all. Throughout the site, the verdicts are colour-coded:

safe derailment conflicting greens collision green into occupied malformed

Simplifications, so the whole state space stays countable on one page: two trains, four track segments, one safety rule-set (the oracle), and — since strings are infinite — wherever a field is a String we audit a small bounded slice of it: five plausible aspect spellings, six plausible positions. Everything else is exhaustive.

Naive representation

-- v0 state
type State =
  { sa :: String
  , sl :: String
  , se :: String
  , sm :: String
  , p1 :: Boolean
  , p2 :: Boolean
  , t1 :: String
  , t2 :: String
  }

The two obvious problems here are:

the String encoding — is it "G", "Green", "green"? what does "" mean? what does "purple" mean? etc etc
Boolean blindness — true here means what? "towards the loop"?

But what does it mean in practice? Let's generate the counter-examples:

Commentary on the naive representation

There are a LOT of ways this can go wrong! Many, many states that would result in disaster, derailment and death in the real world if they occurred. Of the 90,000 values in our bounded slice, 88,400 don't even describe a railway, and another 1,398 describe one in the process of having an accident. The 202 states we actually mean are outnumbered roughly 450 to 1 — and remember, the slice is a courtesy; the real space is infinite.

On the next page we'll start refining this.

Refine the type