Self-contained reference for building on arest. FORML 2 readings compile to a database schema, constraint rules, state machines, and a REST API with HATEOAS, all from one β-reducer over Backus's FFP algebra.
A state machine describes how an entity transitions between statuses. In arest, state machines are first-class FORML 2: you declare them in readings, the compiler produces a transition function, and every call to create or transition folds the current status over the new event.
An SM declaration names the noun it tracks, its initial status, and each transition’s state-machine membership, source status, and target status. Statuses reached by transitions are recognized from those transition facts, so you only need separate Status is defined in State Machine Definition facts for statuses that are not reached by a transition.
State Machine Definition 'Order' is for Noun 'Order'.
Status 'In Cart' is initial in State Machine Definition 'Order'.
Transition 'place' is defined in State Machine Definition 'Order'.
Transition 'place' is from Status 'In Cart'.
Transition 'place' is to Status 'Placed'.
Transition 'ship' is defined in State Machine Definition 'Order'.
Transition 'ship' is from Status 'Placed'.
Transition 'ship' is to Status 'Shipped'.
Both are supported. Verb is performed during Transition X attaches a verb action to a transition (Mealy: output depends on transition). Verb is performed in Status X attaches a verb action to a status (Moore: output depends on current state).
Verb 'notify' is performed during Transition 'place'.
Verb 'send reminder' is performed in Status 'Placed'.
The paper section Facts as Events describes how creating a fact fires an event whose type is the fact type. A transition that declares its trigger as a fact type fires automatically when that fact enters the population.
Transition 'place' is triggered by Event Type 'Order Placed'.
Event Type 'Order Placed' is created by Verb 'place'.
During create, the resolve step pushes facts into P. Each fact push is an event. The machine fold consumes events chronologically. An entity with enough facts to satisfy every outgoing guard can advance from its initial status to its terminal status in a single SYSTEM call.
External events (a webhook, a peer message, a Kafka topic) enter the same stream. The machine does not care whether the event came from a local fact push or an outside source; both are elements of the event sequence E.
The transition function is a chain of conditions (Backus 11.2.4). Given ⟨status, event⟩, it checks each declared transition in order. The first whose predicate matches returns the target status; if none match, the current status is returned unchanged.
transition(s, e) = (p₁ → s'₁ ; (p₂ → s'₂ ; ... ; s)) : ⟨s, e⟩
Invalid events do not raise errors. They simply leave the state unchanged, since a missed transition is a no-op rather than a failure. This matters for event replay: re-applying the event stream to an empty state reproduces the same final status even when some events are redundant.
Some transitions should fire not on a new event but on a condition becoming true. That is a positive guard. Declare it by making the transition’s trigger a fact type that is derived rather than asserted:
Transition 'ship' is triggered by Event Type 'Payment Received'.
When Payment Received is derived (for example, by a rule that watches for sufficient partial payments), the SM fold sees the new fact, the transition matches, and the entity advances.
The runtime’s SM fold runs twice during create: once on the events generated by resolve + derive in chronological order, then a positive-guard loop that scans P for facts matching outgoing transition triggers and fires them until the status is stable.
A status with no outgoing transitions is terminal. Corollary: Deletion says that an entity in a terminal state has links(s) = ∅ and is excluded from query results by restriction.
Status 'Archived' is terminal in State Machine Definition 'Order'.
Transition 'archive' is defined in State Machine Definition 'Order'.
Transition 'archive' is from Status 'Shipped'.
Transition 'archive' is to Status 'Archived'.
Tenants who prefer soft-delete declare an Archived status; those who want hard-delete can retract the facts directly.
Each noun has at most one SM definition. If you need several concurrent workflows on the same entity (an Order has both a payment status and a shipping status), either:
Paid-Pending-Shipment, Paid-Shipped, etc.). Works but explodes.The alethic constraint For each Noun, at most one State Machine Definition is for that Noun. is in the metamodel and will reject multiple SMs on one noun.
Two SMs on different nouns may declare the same status name (e.g. both Domain Change and Merge have a Proposed). The engine disambiguates by the explicit State Machine Definition is for Noun binding — Status 'Proposed' lives in DomainChangeSM for Domain Change entities and in MergeSM for Merge entities. They do not collide.
The disambiguation only works when each SM declares the binding explicitly. A reading like Initial Merge Status is 'Proposed' (without a State Machine Definition is for Noun 'Merge' line) leaves the noun unbound — compile_sm_init_for is per-noun, so no SM init derivation fires for unbound entities. Pinned by compile_picks_dc_sm_for_domain_change_noun_despite_shared_status and compile_picks_merge_sm_for_merge_noun_despite_shared_status in crates/arest/src/compile.rs.
Transition graphs may contain cycles. The metamodel asserts:
It is obligatory that each cycle has some exit transition.
This is a deontic constraint, so your SM is allowed to have a cycle without an exit, but the compiler will warn. If you want a strictly terminating workflow, declare a terminal status and ensure every cycle can reach it.
Transition links are part of Theorem 4: HATEOAS as Projection. The response for an entity includes only the transitions whose from status matches the current one (plus any supertype-inherited transitions).
{
"id": "ord-1",
"status": "Placed",
"_links": {
"ship": { "href": "/orders/ord-1/transition", "method": "POST", "event": "ship" }
}
}
An agent consuming this response sees exactly the valid next moves. Attempting an invalid event (one whose link was not listed) is a no-op by the transition chain, so safety is preserved even when the client is confused.
State machines describe change over time. Derivation rules describe what else follows from the current facts.