Order Lifecycle — the Reference Machine
The one to copy. Every state is reachable from the declared initial state, every transition names states that exist, every fork carries a guard that distinguishes it, every non-final state has a way out, and a run can reach a final state. Retries and cancellations are ordinary cycles and the engine says nothing about them, because a loop is not a defect. Reports clean, and every one of the ten checks says what it covered.
Make it your own.
title "Order lifecycle"
state Cart
state Pending label "Awaiting payment"
state Paid
state Packed
state Shipped
state Delivered final
state Cancelled final
state Refunded final
initial Cart
transition Cart -> Pending on "checkout"
transition Pending -> Paid on "payment" [authorised] / capture
transition Pending -> Pending on "payment" [declined] / notify
transition Pending -> Cancelled on "timeout"
transition Paid -> Packed on "pick"
transition Packed -> Shipped on "dispatch" / send tracking
transition Shipped -> Delivered on "delivered"
transition Paid -> Refunded on "cancel" [not dispatched] / refund
transition Packed -> Refunded on "cancel" [not dispatched] / refund