Skip to main content
The state machine view renders a visual lifecycle diagram for any declared state machine in your model. Navigate to it from an operation’s header (when that operation drives the machine) or from the detail panel of any transition step in the Operation View. The state machine view lives at #/machine/<id>. To link directly to a specific transition — for example, to share a link pointing at the transition a failing obligation names — use #/machine/<id>?t=<transition-id>. Selecting a transition in the graph or table updates the URL, so any link you copy from the address bar is already a deep link. The header shows:
  • The machine’s name and copyable ID
  • The governed object — the data object whose instances this machine tracks
  • The state field path — which field on that object holds the current state
  • The initial state
  • State count and transition count
  • Verdict tally — when a report is loaded, a count of proven/unknown/disproven obligations across all transitions

State graph

The state graph is an SVG diagram with states as nodes and transitions as directed arcs:
  • State nodes are labeled circles. The initial state is marked with an entry arrow.
  • Transition arcs are directed edges connecting a from state to a to state. Transitions that stay on the same state render as self-loops.
  • Side-effect badges (⚡) appear on transition arcs to indicate the number of side effects the transition owns.
Click any state node to open its detail panel. Click or select any transition arc to highlight it in both the graph and the transitions table below; the URL updates to include ?t=<transition-id> for sharing. Clicking a state node without selecting a transition drops the transition query from the URL.

Transitions table

Below the graph, the transitions table lists every declared transition with one row per transition:

Side effects and executors

A transition’s side effects are the publication, request, or external effects it owns. These effects are implicitly established as effect-intent artifacts by the transition step that applies the transition; the operation program later executes them with execute_effect_intent (or execute_effect_intent_async). The transition’s effect_intents map wires side-effect id to { bind, values } for each intent, and the mapping must be exact. Because a transition-containing transaction is never naturally replayable, its containing transaction must declare deduplicated_by for the recovery route to close. The Executors column shows which operations apply this transition and therefore carry responsibility for executing its side effects. Click any operation name in the Executors column to navigate to that operation’s Operation View.

Proof overlays

When a report is loaded, transitions inherit their proof status. A transition whose associated obligations are all proven shows a green verdict chip; any unknown obligation turns it amber; any disproven obligation turns it red. This makes it easy to scan the transitions table for the specific lifecycle steps the checker could not discharge.
Use the ?t=<transition-id> deep link when filing a bug or design discussion. The link opens the machine view with the specific transition pre-selected in both the graph and the table, so your reader lands exactly where you intend.