Transitions

Transitions define how state evolves. Each transition is a pure function: given the current state and an action, it produces a new state. In IML terms, a transition has the signature (state, action) → state.

What a transition looks like

A transition receives s : state and a : action implicitly. The body is an IML expression that returns a new state record. Every field of the state record must be assigned, even fields that don't change:

(* do_deposit: add the deposit amount to the balance *)
{ balance = s.balance + a.amount; status = s.status }

(* do_freeze: change status to Frozen, balance unchanged *)
{ balance = s.balance; status = Frozen }

(* noop: nothing changes *)
{ balance = s.balance; status = s.status }

The requirement to assign every field is deliberate — it makes the effect of each transition completely explicit. There are no implicit "carry forward" semantics. If a field isn't mentioned, the transition won't compile.

Common patterns

Single-effect transitions

Most transitions change one thing:

(* advance_from_red: move to the next phase *)
{ phase = Green }
 
(* do_withdraw: reduce the balance *)
{ balance = s.balance - a.amount; status = s.status }
 
(* do_cancel: zero out and mark cancelled *)
{ total = 0; item_count = 0; discount_applied = s.discount_applied; status = Cancelled }

Branching transitions

When a single handler has branching logic, encode it as one transition with an if expression:

(* on_new_order: accept or reject based on quantity *)
if a.qty > 10000 then
  { pos = s.pos; rejected = s.rejected + 1 }
else
  { pos = s.pos + a.qty; rejected = s.rejected }

Then create one scenario per path through the branches — one scenario for the reject case (with qty_too_big in the when clause) and one for the accept case (with qty_ok).

No-op transitions

A noop transition is a common pattern for rejected or blocked operations:

(* noop: the action is rejected, state doesn't change *)
{ balance = s.balance; status = s.status }

Multiple rejection scenarios can share the same noop transition — withdraw_insufficient, blocked_when_frozen, and modify_after_checkout might all use noop as their then clause.

Nested state updates

For models with nested records, rebuild the full structure:

(* deposit into a multi-module state *)
{ auth = s.auth;
  billing = { balance = s.billing.balance + a.amount; frozen = s.billing.frozen } }

Every field at every level must be assigned.

Transitions vs predicates

Predicates and transitions serve different roles:

Predicates classify; transitions transform. A scenario connects them: given these conditions hold, when this action arrives, then this transformation applies.

Multiple transitions vs one big transition

Use multiple transitions when different operations have distinct handlers:

do_deposit  : { balance = s.balance + a.amount; status = s.status }
do_withdraw : { balance = s.balance - a.amount; status = s.status }
do_freeze   : { balance = s.balance; status = Frozen }
do_unfreeze : { balance = s.balance; status = Active }
noop        : { balance = s.balance; status = s.status }

Use one transition with branching when a single handler dispatches internally:

on_new_order : if a.qty > 10000 then { ... } else { ... }

The deciding factor is the structure of the real system. If the code has separate functions for deposit and withdraw, model them as separate transitions. If the code has one function that branches, model it as one transition with if.

Transitions are shared

Like predicates, transitions are reusable across scenarios:

• noop might be used by withdraw_insufficient, blocked_when_frozen, modify_after_checkout, and modify_after_cancel
• add_item might be used by both add_first_item and add_more_items

Sharing transitions keeps the model consistent — the same transformation is described once and referenced everywhere it applies.

What the reasoning engine checks

When you add or edit a transition, ImandraX performs IML validation:

• Does the expression parse as valid IML?
• Do the referenced fields exist in the domain base types?
• Does the expression return a value of type state?
• Are all fields of the state record assigned?

Each transition is checked independently. If validation fails, the transition is marked invalid and any scenario that references it cannot be fully analyzed.

Since IML compiles to executable code via ImandraX, transitions aren't just specifications — they're runnable functions that can be evaluated against concrete inputs during analysis.

See Consistency checking for more on how transitions are validated.