State

Syntax

state: <StateName> | <StateName>(<field>: <Type>, ...)

States are declared inline within a decider block using the state: label. Multiple states are separated by | (union).

Parameterized States

States can carry data via typed fields:

state: Empty | Active(items: ItemList, discount: Boolean) | CheckedOut(orderId: OrderId)

Fieldless states (like Empty) represent conditions with no associated data.

Initial State

The initial state is declared in the decider header with initial::

initial: Empty

The initial state must be fieldless (no parameters). The grammar enforces exactly one initial state per decider.

Terminal States

Terminal states are declared in the decider header with terminal::

terminal: CheckedOut
terminal: Closed, Cancelled

Terminal states are absorbing — no further commands are accepted once the system enters one. Multiple terminal states are separated by commas. See Decider reference for terminal state semantics.

Scope

States are scoped to their enclosing decider. They are referenced by decide, evolve, initial:, and terminal: declarations within that decider.

Example

decider ShoppingCart {
    commands: OpenCart, AddItem, Checkout
    events: CartOpened, ItemAdded, OrderPlaced
    state: Empty | Active(items: ItemList) | CheckedOut(orderId: OrderId)
    initial: Empty
    terminal: CheckedOut

    // ... decide and evolve clauses ...
}

Compiler Checks

Check	What It Verifies
Exhaustiveness	Every non-terminal state has a decide clause for every command
Evolve totality	Every non-terminal state has an evolve clause for every event
Terminal enforcement	Terminal states are excluded from cross-product checks