Traffic Lights
A simple example demonstrating basic state machine concepts with a traffic light controller.
Basic Traffic Light
flow
machine: @traffic_light
scenario: normal operation
given:
traffic_light is in #red
on :timer_expired from @system
? traffic_light is in #red
traffic_light moves to #green
start timer for 30 seconds
? traffic_light is in #green
traffic_light moves to #yellow
start timer for 5 seconds
? traffic_light is in #yellow
traffic_light moves to #red
start timer for 30 seconds
expect:
= traffic light cycles correctlyWith Pedestrian Crossing
flow
machine: @traffic_light
scenario: pedestrian crossing
given:
traffic_light is in #red
$pedestrian_waiting: boolean is false
on> :pedestrian_button_pressed from @pedestrian
$pedestrian_waiting becomes true
? traffic_light is in #green
start shortened green timer
on :timer_expired from @system
? traffic_light is in #red
? $pedestrian_waiting
traffic_light moves to #pedestrian_crossing
start timer for 20 seconds
$pedestrian_waiting becomes false
otherwise
traffic_light moves to #green
start timer for 30 seconds
? traffic_light is in #pedestrian_crossing
traffic_light moves to #green
start timer for 30 seconds
? traffic_light is in #green
traffic_light moves to #yellow
start timer for 5 seconds
? traffic_light is in #yellow
traffic_light moves to #red
start timer for 30 seconds
expect:
= pedestrians can cross safelyIntersection Controller
flow
system: intersection
machine: @north_south_light
on :switch_to_green from @controller
light moves to #green
start timer for 30 seconds
on :timer_expired from @system
? light is in #green
light moves to #yellow
start timer for 5 seconds
? light is in #yellow
light moves to #red
emit :ns_is_red to @controller
machine: @east_west_light
on :switch_to_green from @controller
light moves to #green
start timer for 30 seconds
on :timer_expired from @system
? light is in #green
light moves to #yellow
start timer for 5 seconds
? light is in #yellow
light moves to #red
emit :ew_is_red to @controller
machine: @controller
scenario: coordinate lights
given:
@north_south_light is in #green
@east_west_light is in #red
on :ns_is_red from @north_south_light
// Wait 2 seconds for safety
wait 2 seconds
emit :switch_to_green to @east_west_light
on :ew_is_red from @east_west_light
// Wait 2 seconds for safety
wait 2 seconds
emit :switch_to_green to @north_south_light
expect:
= only one direction is green at a timeState Diagram
@traffic_light
┌─────────────────────────────────────────────┐
│ │
│ ┌─────────┐ :timer ┌─────────┐ │
│ │ #red │ ─────────────────>│ #green │ │
│ └────▲────┘ └────┬────┘ │
│ │ │ │
│ │ :timer │
│ :timer │ │
│ │ ▼ │
│ │ ┌─────────┐ │
│ └────────────────────────│ #yellow │ │
│ └─────────┘ │
│ │
└─────────────────────────────────────────────┘
Cycle: #red → #green → #yellow → #redWith Pedestrian State
@traffic_light
┌──────────────────────────────────────────────────┐
│ │
│ ┌─────────┐ ┌─────────┐ │
│ │ #red │ ────────────────────>│ #green │ │
│ └────┬────┘ └────┬────┘ │
│ │ │ │
│ │ [pedestrian waiting] :timer │
│ │ │ │
│ ▼ ▼ │
│ ┌────────────────────┐ ┌─────────┐ │
│ │#pedestrian_crossing│ │ #yellow │ │
│ └─────────┬──────────┘ └────┬────┘ │
│ │ │ │
│ :timer :timer │
│ │ │ │
│ └──────────────────────────┘ │
│ │ │
│ ▼ │
│ [back to #red] │
│ │
└──────────────────────────────────────────────────┘Lane Diagram (Intersection)
┌─────────────┬─────────────┬─────────────┐
│ @controller │ @ns_light │ @ew_light │
├─────────────┼─────────────┼─────────────┤
│ │ │ │
│ │ ● #green │ ○ #red │
│ │ │ │
│ │ :timer │ │
│ │ ──────────> │ │
│ │ │ │
│ │ ● #yellow │ │
│ │ │ │
│ │ :timer │ │
│ │ ──────────> │ │
│ │ │ │
│ :ns_is_red │ ● #red │ │
│ <───────────┼─────────────│ │
│ │ │ │
│ [wait 2s] │ │ │
│ │ │ │
│ :switch_ │ │ │
│ to_green │ │ │
│ ────────────┼─────────────┼──> │
│ │ │ │
│ │ │ ● #green │
│ │ │ │
└─────────────┴─────────────┴─────────────┘Testing Scenarios
Normal Cycle
flow
scenario: complete cycle
given:
traffic_light is in #red
on :timer_expired from @system
traffic_light moves to #green
on :timer_expired from @system
traffic_light moves to #yellow
on :timer_expired from @system
traffic_light moves to #red
expect:
= traffic_light is in #red
= cycle completed successfullyPedestrian Interruption
flow
scenario: pedestrian requests crossing
given:
traffic_light is in #green
$pedestrian_waiting is false
on> :pedestrian_button_pressed from @pedestrian
$pedestrian_waiting becomes true
on :timer_expired from @system
traffic_light moves to #yellow
on :timer_expired from @system
traffic_light moves to #red
on :timer_expired from @system
? $pedestrian_waiting
traffic_light moves to #pedestrian_crossing
expect:
= traffic_light is in #pedestrian_crossing
= $pedestrian_waiting is falseIntersection Safety
flow
scenario: lights never both green
given:
@north_south_light is in #green
@east_west_light is in #red
on :timer_expired from @system
@north_south_light moves to #yellow
on :timer_expired from @system
@north_south_light moves to #red
on :ns_is_red from @north_south_light
// Controller waits, then switches
on :switch_to_green from @controller
@east_west_light moves to #green
expect:
= @north_south_light is in #red
= @east_west_light is in #green
= never both green simultaneouslyKey Concepts Demonstrated
- Simple state transitions - Traffic light cycles through states
- Timer-based triggers - State changes on timer expiration
- Guard conditions - Check current state before transitioning
- Multi-machine coordination - Controller synchronizes lights
- Safety invariants - Ensure conflicting states never occur simultaneously