Order State Flow
The companion executable model for E-Commerce Order State Machine in TLA+.
Four state machines run at once, and the fourth is not independent:
| Machine | States | Role |
|---|---|---|
| order | 7 | checkout progression |
| payment | 8 | independent lifecycle |
| shipment | 11 | fulfillment lifecycle |
| status | 9 | derived customer-facing status |
The point of the spec is that status is a function of the other three, not a
field someone remembers to update. Most order-system bugs are a payment or
shipment transition that fails to propagate – an order showing "Delivered"
against a refunded payment. Deriving the customer-facing status makes that class
of bug unrepresentable rather than merely tested-for.
The model carries 28 transitions and 11 invariants, plus 7 named failure scenarios.
Drift risk
The TLA+ shown in the viewer is a hardcoded string outside this core. Nothing checks that the displayed spec text and the executable model agree. Same known parity risk as Gas Town.
Status
Core-only. app.cljs is a stub; there is no UI on this page yet.
| Piece | Namespace | State |
|---|---|---|
| Pure logic | wal-sh.projects.order-state-flow.core |
complete |
| Storage | wal-sh.projects.order-state-flow.storage |
complete |
| SPA entry | wal-sh.projects.order-state-flow.app |
stub |
27 example-based tests and 4 test.check properties are defined under
test/wal_sh/projects/order_state_flow/.