Completeness Checks

Exhaustiveness Check

Every non-terminal state must have a decide clause for every command declared in the decider.

For a decider with commands [OpenCart, AddItem] and non-terminal states [Empty, Active], the compiler checks all 4 pairs:

	Empty	Active
OpenCart	required	required
AddItem	required	required

Missing pairs produce errors with actionable messages:

Missing decide clause for (AddItem, Empty) in decider ShoppingCart.
Add: decide(AddItem, Empty) -> [...]

Formal Basis

The decide function maps Command × State → Result<Events[], RejectionError>. Exhaustiveness ensures this function is total over its domain — every input pair has a defined output.

Evolve Totality Check

Every non-terminal state must have an evolve clause for every event declared in the decider.

For a decider with events [CartOpened, ItemAdded, CartEmptied] and non-terminal states [Empty, Active], the compiler checks all 6 pairs:

	Empty	Active
CartOpened	required	required
ItemAdded	required	required
CartEmptied	required	required

Missing pairs produce errors:

Missing evolve clause for (Active, CartEmptied) in decider ShoppingCart.
Add: evolve(Active, CartEmptied) -> <TargetState>

Why Every Pair Matters

A single decide clause can emit multiple events: -> [ItemRemoved, CartEmptied]. These events are applied via left-fold — each evolve receives the intermediate state produced by the previous one. The entire sequence is atomically committed.

For decide(RemoveItem, Active) -> [ItemRemoved, CartEmptied]:

1. evolve(Active, ItemRemoved) must exist — produces Active
2. evolve(Active, CartEmptied) must exist — produces Empty

If step 1 produced a different state variant, step 2 would need a matching evolve for that variant. The cross-product check ensures all reachable intermediate states are covered.

Formal Basis

The evolve function is an F-algebra α: State × Event → State. Totality means α is defined on all elements of its domain. Since states form a finite algebraic data type, the compiler can statically verify this property without executing the code.

Terminal State Enforcement

States marked terminal(StateName) = true in a decider are absorbing states. Once the system enters a terminal state, no further commands are accepted and no further transitions occur. Common examples: CheckedOut in a shopping cart, Closed in a support ticket.

Exclusion from Exhaustiveness and Totality

The compiler excludes terminal states from both the exhaustiveness and evolve totality cross-products. Only non-terminal states require decide and evolve clauses.

Exhaustiveness: A decider with commands [Open, Close, Reopen], states [New, Active, Closed], and terminal(Closed) = true requires 6 decide clauses (3 commands × 2 non-terminal states), not 9.

Evolve totality: The same exclusion applies — only non-terminal states require evolve clauses for each event.

The cross-product for the example above:

	New	Active	Closed
Open	required	required	excluded
Close	required	required	excluded
Reopen	required	required	excluded

A concrete decider using this exclusion:

decider Ticket {
    commands: Open, Close, Reopen
    events:   Opened, TicketClosed, Reopened
    state:    New | Active | Closed

    decide(Open, New) -> [Opened]
    decide(Close, New) -> [TicketClosed]
    decide(Close, Active) -> [TicketClosed]
    decide(Reopen, New) -> [Reopened]
    decide(Reopen, Active) -> [Reopened]
    // No decide clauses needed for (*, Closed)

    evolve(New, Opened) -> Active
    evolve(New, TicketClosed) -> Closed
    evolve(Active, TicketClosed) -> Closed
    evolve(New, Reopened) -> Active
    evolve(Active, Reopened) -> Active
    // No evolve clauses needed for (Closed, *)

    terminal(Closed) = true
}

Implementation

Both checkDeciderExhaustiveness and checkEvolveTotality collect terminal state names from TerminalDecl members where value === 'true', then filter the state list to non-terminal states before computing the cross-product. The exclusion happens at the point of set construction — terminal states are never placed into the required-pairs matrix.

Future Enforcement

The allium spec (validation-terminal-states.allium) describes additional enforcement in the code generation phase: generated deciders must return Err(RejectionError) for every command when the current state is terminal. This is a generator-phase concern, not yet implemented.

Two further validation-phase checks are planned but not yet specced in allium:

• No decide clause should target a terminal state — such a clause is dead code because the state can never receive a command at runtime.
• At least one non-terminal state must exist — a decider composed entirely of terminal states accepts no commands and therefore has no defined behaviour.