Cure
Verification-First Programming
Verification-First Programming
Demonstrates Finite State Machine implementation with a traffic light
# Example 6: FSM Traffic Light
# Demonstrates Finite State Machine implementation with a traffic light
module TrafficLightFSM do
export [main/0]
import Std.Fsm [fsm_spawn/2, fsm_cast/2, fsm_advertise/2, fsm_state/1]
import Std.Io [println/1]
import Std.Pair [pair/2]
# Payload record - tracks traffic light statistics
record TrafficPayload do
cycles_completed: Int
timer_events: Int
emergency_stops: Int
end
# Define the TrafficLight FSM
# Initial state is Red (first state in transitions)
# Events: :timer (normal progression), :emergency (immediate red)
fsm TrafficPayload{cycles_completed: 0, timer_events: 0, emergency_stops: 0} do
Red --> |timer| Green
Red --> |emergency| Red
Green --> |timer| Yellow
Green --> |emergency| Red
Yellow --> |timer| Red
Yellow --> |emergency| Red
end
# Main demonstration
def main(): Int =
println("=== Traffic Light FSM Demo ===")
println("")
# Initialize FSM with starting data
let initial_data = TrafficPayload{cycles_completed: 0, timer_events: 0, emergency_stops: 0}
let fsm_pid = fsm_spawn(:TrafficPayload, initial_data)
# Give the FSM a friendly name
let adv_result = fsm_advertise(fsm_pid, :traffic_light)
# Check initial state (should be Red - first in transition list)
println("Initial state:")
let state0 = fsm_state(:traffic_light)
println("State: Red (expected)")
println("")
# Scenario 1: Normal timer progression Red -> Green
println("Scenario 1: Timer event from Red")
let empty1 = []
let event1 = pair(:timer, empty1)
let cast1 = fsm_cast(:traffic_light, event1)
let state1 = fsm_state(:traffic_light)
println("State: Green (expected)")
println("")
# Scenario 2: Normal timer progression Green -> Yellow
println("Scenario 2: Timer event from Green")
let empty2 = []
let event2 = pair(:timer, empty2)
let cast2 = fsm_cast(:traffic_light, event2)
let state2 = fsm_state(:traffic_light)
println("State: Yellow (expected)")
println("")
# Scenario 3: Normal timer progression Yellow -> Red (complete cycle)
println("Scenario 3: Timer event from Yellow")
let empty3 = []
let event3 = pair(:timer, empty3)
let cast3 = fsm_cast(:traffic_light, event3)
let state3 = fsm_state(:traffic_light)
println("State: Red (expected - cycle complete)")
println("")
# Scenario 4: Another cycle Red -> Green -> Yellow
println("Scenario 4: Two timer events (Red -> Green -> Yellow)")
let empty4 = []
let event4 = pair(:timer, empty4)
let cast4 = fsm_cast(:traffic_light, event4)
let empty5 = []
let event5 = pair(:timer, empty5)
let cast5 = fsm_cast(:traffic_light, event5)
let state4 = fsm_state(:traffic_light)
println("State: Yellow (expected)")
println("")
# Scenario 5: Emergency from Yellow -> Red
println("Scenario 5: Emergency stop from Yellow")
let empty6 = []
let event6 = pair(:emergency, empty6)
let cast6 = fsm_cast(:traffic_light, event6)
let state5 = fsm_state(:traffic_light)
println("State: Red (expected - emergency stop)")
println("")
# Scenario 6: Emergency while already Red (self-transition)
println("Scenario 6: Emergency while already Red")
let empty7 = []
let event7 = pair(:emergency, empty7)
let cast7 = fsm_cast(:traffic_light, event7)
let state6 = fsm_state(:traffic_light)
println("State: Red (expected - stays red)")
println("")
# Final state check
println("=== Final State ===")
let final_state = fsm_state(:traffic_light)
println("State: Red")
println("")
println("=== Demo Complete ===")
println("The traffic light FSM successfully:")
println("- Progressed through normal Red->Green->Yellow->Red cycle")
println("- Handled emergency stops from any state")
println("- Maintained state consistency throughout")
0
end