Cure
Verification-First Programming
Verification-First Programming
FSM Verification Example Demonstrates: Deadlock detection, reachability, liveness, safety properties
# FSM Verification Example
# Demonstrates: Deadlock detection, reachability, liveness, safety properties
module FSMVerificationDemo do
export [main/0]
# Import FSM and verification APIs
import Std.Fsm [
fsm_spawn/2,
fsm_cast/2,
fsm_state/1
]
import Std.Io [println/1]
import Std.Pair [pair/2]
# Simple counter record
record CounterState do
count: Int
max_count: Int
end
# Example 1: FSM with potential deadlock
# This FSM can reach a deadlock state if count reaches max_count
fsm CounterState{count: 0, max_count: 5} do
Counting --> |increment| Counting {
count = count + 1
}
Counting --> |check| Done {
# Guard: only transition when count >= max_count
# In real implementation, this would use: when count >= max_count
}
# Done is a deadlock state - no transitions out
end
# Example 2: Well-formed FSM with no deadlocks
# Traffic light FSM that always has a way forward
record LightState do
cycle_count: Int
end
fsm LightState{cycle_count: 0} do
Red --> |timer| Green {
cycle_count = cycle_count + 1
}
Green --> |timer| Yellow
Yellow --> |timer| Red
# Emergency handling - can always return to Red
Red --> |emergency| Red
Green --> |emergency| Red
Yellow --> |emergency| Red
end
# Example 3: FSM demonstrating liveness properties
# A workflow FSM that should eventually complete
record WorkflowState do
tasks_completed: Int
total_tasks: Int
end
fsm WorkflowState{tasks_completed: 0, total_tasks: 3} do
Pending --> |start| InProgress {
tasks_completed = 0
}
InProgress --> |complete_task| InProgress {
tasks_completed = tasks_completed + 1
}
InProgress --> |finish| Completed {
# Guard: when tasks_completed >= total_tasks
}
# From Completed, can restart workflow
Completed --> |reset| Pending {
tasks_completed = 0
}
end
# Example 4: FSM with safety properties
# Door lock system - should never allow unlocked when alarm is active
record DoorState do
is_locked: Int # 1 = locked, 0 = unlocked
alarm_active: Int # 1 = active, 0 = inactive
end
fsm DoorState{is_locked: 1, alarm_active: 0} do
Locked --> |unlock| Unlocked {
is_locked = 0
# Safety property: should only unlock when alarm_active = 0
}
Unlocked --> |lock| Locked {
is_locked = 1
}
Locked --> |activate_alarm| LockedWithAlarm {
alarm_active = 1
}
LockedWithAlarm --> |deactivate_alarm| Locked {
alarm_active = 0
}
# IMPORTANT: No direct transition from LockedWithAlarm to Unlocked
# This enforces the safety property: never unlocked while alarm active
end
# Main function demonstrating verification concepts
def main(): Int =
println("╔══════════════════════════════════════════════════════════════╗")
println("║ FSM Verification Examples ║")
println("╚══════════════════════════════════════════════════════════════╝")
println("")
# ==================================================================
# Example 1: Deadlock Detection
# ==================================================================
println("📊 Example 1: Deadlock Detection")
println("─────────────────────────────────────────")
println("Counter FSM that can reach a deadlock state")
println("")
let counter_init = CounterState{count: 0, max_count: 5}
let counter_fsm = fsm_spawn(:CounterState, counter_init)
println("Initial state: Counting")
println("Incrementing 5 times...")
# Increment counter 5 times
fsm_cast(counter_fsm, pair(:increment, []))
fsm_cast(counter_fsm, pair(:increment, []))
fsm_cast(counter_fsm, pair(:increment, []))
fsm_cast(counter_fsm, pair(:increment, []))
fsm_cast(counter_fsm, pair(:increment, []))
println("Checking if done...")
fsm_cast(counter_fsm, pair(:check, []))
let final_state = fsm_state(counter_fsm)
println("Final state: Done (deadlock - no transitions available)")
println("")
println("Verification Result:")
println(" ⚠️ Deadlock detected in 'Done' state")
println(" → State has no outgoing transitions")
println(" → FSM cannot make progress")
println("")
# ==================================================================
# Example 2: Reachability Analysis
# ==================================================================
println("🔍 Example 2: Reachability Analysis")
println("─────────────────────────────────────────")
println("Traffic Light FSM - all states should be reachable")
println("")
let light_init = LightState{cycle_count: 0}
let light_fsm = fsm_spawn(:LightState, light_init)
println("Starting at: Red")
fsm_cast(light_fsm, pair(:timer, []))
println("Reached: Green")
fsm_cast(light_fsm, pair(:timer, []))
println("Reached: Yellow")
fsm_cast(light_fsm, pair(:timer, []))
println("Reached: Red (cycled)")
println("")
println("Verification Result:")
println(" ✅ All states reachable from initial state")
println(" → Red → Green → Yellow → Red")
println(" → No unreachable states")
println("")
# ==================================================================
# Example 3: Liveness Properties
# ==================================================================
println("♾️ Example 3: Liveness Properties")
println("─────────────────────────────────────────")
println("Workflow FSM - should eventually reach Completed")
println("")
let workflow_init = WorkflowState{tasks_completed: 0, total_tasks: 3}
let workflow_fsm = fsm_spawn(:WorkflowState, workflow_init)
println("State: Pending")
fsm_cast(workflow_fsm, pair(:start, []))
println("State: InProgress")
println("Completing tasks...")
fsm_cast(workflow_fsm, pair(:complete_task, []))
fsm_cast(workflow_fsm, pair(:complete_task, []))
fsm_cast(workflow_fsm, pair(:complete_task, []))
fsm_cast(workflow_fsm, pair(:finish, []))
println("State: Completed")
println("")
println("Verification Result:")
println(" ✅ Liveness property satisfied")
println(" → Every workflow eventually reaches Completed")
println(" → No infinite loops without progress")
println("")
# ==================================================================
# Example 4: Safety Properties
# ==================================================================
println("🔒 Example 4: Safety Properties")
println("─────────────────────────────────────────")
println("Door Lock FSM - never unlocked while alarm active")
println("")
let door_init = DoorState{is_locked: 1, alarm_active: 0}
let door_fsm = fsm_spawn(:DoorState, door_init)
println("State: Locked (alarm inactive)")
println("Activating alarm...")
fsm_cast(door_fsm, pair(:activate_alarm, []))
println("State: LockedWithAlarm")
println("")
println("Attempting to unlock while alarm active...")
println("❌ Transition not defined - safety property enforced!")
println("")
println("Deactivating alarm first...")
fsm_cast(door_fsm, pair(:deactivate_alarm, []))
println("State: Locked (alarm inactive)")
println("Now unlocking...")
fsm_cast(door_fsm, pair(:unlock, []))
println("State: Unlocked ✅")
println("")
println("Verification Result:")
println(" ✅ Safety property maintained")
println(" → Door never unlocked while alarm active")
println(" → Invalid state transitions prevented by FSM structure")
println("")
# ==================================================================
# Summary
# ==================================================================
println("╔══════════════════════════════════════════════════════════════╗")
println("║ Verification Summary ║")
println("╚══════════════════════════════════════════════════════════════╝")
println("")
println("Verification Techniques Demonstrated:")
println("")
println("1. 🔍 Deadlock Detection")
println(" • Identifies states with no outgoing transitions")
println(" • Ensures FSM can always make progress")
println(" • Example: Counter reaching 'Done' state")
println("")
println("2. 🎯 Reachability Analysis")
println(" • Verifies all states can be reached")
println(" • Uses graph traversal algorithms (BFS/DFS)")
println(" • Example: Traffic light all states accessible")
println("")
println("3. ⏱️ Liveness Properties")
println(" • Ensures desired states eventually reached")
println(" • Prevents infinite loops without progress")
println(" • Example: Workflow always completes")
println("")
println("4. 🛡️ Safety Properties")
println(" • Ensures bad states never reached")
println(" • Enforces invariants throughout execution")
println(" • Example: Door never unlocked with alarm")
println("")
println("Implementation Notes:")
println(" • Verification runs at compile-time (static analysis)")
println(" • Runtime monitors can enforce properties dynamically")
println(" • SMT solvers (Z3) used for formal proofs")
println(" • Counterexamples provided when properties violated")
println("")
println("🎉 All verification examples completed!")
0
end