Specifying Behaviour as a State Machine with Guards

Prose specifications of event-driven behaviour fail in a specific way: they describe each event in isolation and leave the combinations unstated. A document that says “an order can be cancelled before it ships” and separately “a refund is issued when an order is cancelled” does not say what happens when cancellation arrives after shipment, whether a second cancellation is an error or a no-op, or whether a refund can be issued twice. A transition table forces those questions, because a table has to have an answer in every cell or an explicit marker for the cells that have none.

The formalism is old and small. A state machine is a finite set of states $S$, a finite set of events $E$, a transition relation $\delta \subseteq S \times E \times S$, a designated initial state, and optionally a set of accepting or terminal states. The moment the relation is written as a function rather than a relation — one target state per (state, event) pair — determinism becomes a property that can be checked rather than assumed. The moment guards are added, the function becomes partial and the specification has to say what happens outside its domain.

Guards, and the order dependence they create

A guard is a predicate on state and event payload that must hold for a transition to fire. Guards are what make a table expressible without enumerating every combination of payload values as separate states. A payment transition might fire on authorize only when the amount is within the remaining balance; otherwise a different transition handles the over-balance case.

The trouble is that guards turn a deterministic table into a set of rules that may overlap. If two transitions from the same state accept the same event and both guards hold, the behaviour depends on evaluation order. That is a specification defect, not an implementation detail: two implementations that scan the rule list in different orders will disagree on observable behaviour, and neither is wrong relative to the document.

Two disciplines fix this. The first is to require guards on transitions from the same state to be mutually exclusive, and to prove it: for any two guards $g_1, g_2$ on the same (state, event) pair, the conjunction $g_1 \wedge g_2$ must be unsatisfiable. For simple predicates over integers and enums this is a decidable check, and a table with a few dozen guards can be checked exhaustively over a bounded input domain. The second discipline accepts overlap but declares priority, in which case the priority order is part of the specification and must be documented alongside the guards, because a reader cannot reconstruct it from the table alone.

A related trap is the guard that reads state the event does not carry. If a transition’s guard depends on a clock, on a counter maintained elsewhere, or on a value fetched from a remote service, then the machine is no longer a state machine over the declared state set. It is a machine over state plus environment, and its behaviour is not reproducible from the declared inputs. Specifications that need time usually model it as an explicit event — a timer expiry delivered into the machine — rather than as a predicate the machine reads. That keeps the state set closed and makes the ordering of timeouts an explicit part of the design.

Completeness, and the events a table forgets

A table is complete when every (state, event) pair either has a transition or is explicitly marked as an error or as ignored. Completeness is not a stylistic preference. An unmarked cell is an unspecified behaviour, and unspecified behaviour in a protocol is where implementations diverge.

The usual failure is not a missing row for a known event; it is a missing event. A specification lists the events the designer had in mind, and then reality delivers a duplicate, a late arrival, or a message from a peer that has already moved on. Duplicate delivery is the canonical case: any transport that retries can deliver the same event twice, so a machine with a transition on submit needs a decision about a second submit in the same state. Either it is idempotent, or it is an error, or it transitions somewhere new. All three are legitimate; leaving the cell blank is not.

Marking the cells also exposes the error-handling budget. A table in which every unexpected event raises a fatal error is a specification that says the system has no recovery path. A table in which every unexpected event is silently ignored is a specification that says nothing can go wrong. Most real designs have a third category — events that are ignored because they are stale, distinguished from events that are rejected because they are invalid — and the distinction only becomes visible when the ignored cells are written down with a reason attached.

Terminal states deserve the same treatment. A state with no outgoing transitions is a claim that the entity is finished. If a later requirement needs to reopen a cancelled order, the claim was wrong, and the cost of discovering that is a change to the state set rather than to a single rule. Specifications often mark a state terminal by omission rather than by declaration, which makes the claim invisible and therefore easy to violate accidentally.

Reachability and the states nobody can enter

Once the table is complete, it can be analysed as a graph. The set of states reachable from the initial state by any sequence of events is computable by breadth-first traversal in time linear in the size of the transition relation. Any state outside that set is dead: it has an entry in the table, it may have outgoing transitions, and no execution can ever arrive there.

Unreachable states are almost always a symptom of a modelling error rather than harmless redundancy. Three causes recur. The first is a guard that can never hold, usually because it contradicts a state invariant or because two conditions in the same conjunction are mutually exclusive. The second is a transition into a state that is later removed from the reachable set by a change elsewhere in the table — an orphan left by editing. The third is a state that the designer believed was reachable through an event the table does not actually accept from any predecessor.

The reverse check matters as much: every state must be able to reach a terminal state, or the machine has a livelock. A state from which no terminal state is reachable traps the entity permanently, and in a workflow with external side effects that trap becomes an operational problem rather than a specification curiosity.

def reachable(states, initial, delta):
    seen, stack = {initial}, [initial]
    while stack:
        s = stack.pop()
        for (src, event), dst in delta.items():
            if src == s and dst not in seen:
                seen.add(dst)
                stack.append(dst)
    return seen

dead = set(states) - reachable(states, initial, delta)

The traversal above treats guards as uninterpreted, so it computes the over-approximation: a state it reports as reachable may still be unreachable because no assignment of payload satisfies the guards on the path. Proving the tighter result requires reasoning about the guards, which is where the analysis stops being a five-line script and starts being a satisfiability question. The over-approximation is still useful, because a state it reports as dead is certainly dead.

Where the table stops being the right tool

A flat table has $|S| \times |E|$ cells, and both factors grow. Adding one orthogonal concern — a payment lifecycle that runs alongside a fulfilment lifecycle — multiplies the state count by the product of the two machines rather than adding to it. That is the state explosion that motivates hierarchical and parallel state machines, the notation Harel introduced as statecharts, where a composite state contains sub-machines and events are handled by the innermost active machine that accepts them.

Hierarchy does not remove the specification work; it relocates it. The question of what happens when an event arrives at a composite state whose substates disagree becomes a question about exit and entry ordering, and that ordering must be specified explicitly or implementations will differ on whether an exit action runs before or after the parent’s transition. The same discipline that produced a complete flat table produces a complete hierarchy, with the additional obligation to state the precedence rule once.

The table’s real contribution is not the diagram. It is that every cell is a question someone had to answer, and every unanswerable cell is a requirement that was never settled. A specification that survives contact with a table has already had most of its ambiguities removed, which is why the exercise is worth doing even when the resulting artefact is thrown away. What remains after the table is the part that no table captures: the invariants that must hold across all states, which are the subject of inductive invariants over reachable states, and the failure semantics of transitions that involve another system, covered in partial failure and retry semantics.