Vending Machine Explorer

Interact with the machine and watch the state machine, invariants, and transition formulas update in real time.

Idle Authorized ChoiceReady Executing Delivered Resetting reject coin ready select vend take Step: 0
$0.00
INSERT COINS

Current State

σ.state = Idle

Variables

Invariants

Last Transition

— waiting for first action

Transition History

0Initσ := (Idle, credit=0, choice=∅, delivered=false)