AN INTERSECTION, FOUR PROMISES

The promise of a green light

Try a controller. Watch what happens. Then check every state it can reach.

North greenTick 0
Two crossing roadsNorth–south and east–west through movements, with a signal for each road. Text below reports the signal colors. CROSSINGZONE NORTH–SOUTHEAST–WEST
N–S GreenE–W Red

CONTROLLER 04

Take turns.

Each change adds 2 yellow ticks and 1 red-clearance tick. Ticks are abstract, not seconds.

EXHAUSTIVE CHECK

Beyond the animation

The checker explores all four detector inputs at every reachable state, including inputs you did not select above.

Run the check to see what this controller guarantees.

What does this check assume?

Two incompatible through movements; atomic state changes; a clock that keeps ticking; lamps that exactly follow the model. It checks simultaneous green and recurring green service. It does not model cars inside the crossing, turning traffic, pedestrians, hardware, or collisions. A green opportunity does not mean every queued vehicle gets through.