Specify states, transitions, safety, and liveness

A loop becomes reason-able when it is expressed as a transition system rather than scattered callbacks. Let S be the set of states, E the set of events, and T a next-state relation. A transition consumes a current state and an accepted event, checks a guard, and produces a new state plus zero or more commands. The command describes an intended effect; a later event reports what actually happened. Keeping the reducer pure prevents an in-memory assignment from masquerading as a completed external action.

State should contain only durable facts needed to choose or verify future transitions: lifecycle phase, identifiers, version, observed resources, approvals, budgets, attempts, deadlines, effect receipts, and terminal reason. Large documents and traces can live in referenced immutable artifacts. Derived values such as “is expired” can be computed from a recorded deadline and an injected clock. If two replicas read the same state and event, the reducer should produce the same next state and commands.

Events are facts stated in past tense: request_admitted, evidence_recorded, approval_granted, command_dispatched, effect_confirmed, deadline_reached, or cancellation_received. Commands are imperatives: fetch_order, create_refund, start_test, or notify_operator. A proposed command is not an event. Recording “refund_created” before the payment service confirms it destroys the distinction needed to recover from timeouts. Conversely, store a dispatch intent before execution when the system must not lose work between commitment and delivery.

Guards encode eligibility. An approval transition may require authenticated identity, a matching artifact digest, an allowed role, and an unexpired deadline. Put guards in trusted reducer or policy code, not in prose. Illegal state-event pairs should be rejected or converted into explicit ignored-event records; silently accepting them makes invariants untestable. A transition table is often more useful than a flowchart because it lists source state, event, guard, target state, command, and invariant impact.

Safety properties say that something bad never happens. Examples: at most one refund receipt exists; a write never precedes authorization; terminal state never returns to active; consumed budget never decreases; an approved artifact digest equals the executed artifact digest. Liveness properties say that something good eventually happens under assumptions: every admitted run eventually becomes terminal if dependency responses or deadlines are eventually delivered. Safety is usually unconditional within the controller. Liveness must name fairness and environment assumptions or it becomes impossible to prove.

A state invariant is a predicate true in the initial state and preserved by every transition. Instead of reviewing the happy path, review each transition against each invariant. If approval is required before execute, transitions into executing must establish a valid approval and every transition out must preserve or consume it correctly. This local proof style scales better than mentally simulating every path.

Harel's statecharts introduced hierarchy, concurrency, and broadcast communication to manage state explosion in reactive systems. Hierarchy is useful when many phases share behavior. An active superstate may contain gathering, planning, and executing substates while a cancellation event is handled once at the superstate boundary. Orthogonal regions can model concurrent concerns such as lifecycle and approval. Use them carefully: hidden cross-region coupling can be harder to understand than an explicit product state.

Terminal states deserve the same precision as active states. Define succeeded, rejected, cancelled, expired, exhausted, compensated, quarantined, and needs_operator where relevant. Attach a structured reason and last verified external state. “Failed” alone cannot tell an operator whether retry is safe. Terminal does not necessarily mean data is deleted; it means the controller will take no further effect without a new external event or a new run.

Loops also need monotonic fields. State version increments; consumed budgets do not decrease; approvals move from absent to granted to consumed or expired; effect status advances from intended to dispatched to confirmed or ambiguous, never backward without an explicit compensation record. Monotonicity limits contradictory histories and supports safe comparison when events arrive out of order. If an old observation arrives after a new one, its source version or timestamp lets the reducer ignore it without erasing newer truth.

Model checking explores transition interleavings against properties. TLA+ describes behavior as sequences of states, an initial predicate, and a next-state relation. A small abstraction can uncover duplicate delivery, cancellation races, stale approvals, and missing terminal paths long before implementation tests enumerate them. The model should omit irrelevant payload detail while preserving lifecycle, authority, and concurrency. A counterexample is a concrete trace, not a theoretical embarrassment; translate it into a regression test and a design correction.

Formalization is valuable even without a proof tool. Writing variables, initial values, actions, invariants, liveness goals, and environment assumptions forces ambiguous English into reviewable claims. The aim is not mathematical decoration. It is to ensure every reachable state has a defined owner, legal next events, bounded waiting behavior, and an explanation an operator can act on.