Predicates

Predicates are classifications, not behavior. They answer "what is true?" about a state or action. They are the building blocks that scenarios are composed from.

Two kinds of predicates

State predicates

A state predicate classifies the current state. It receives s : state implicitly and returns a boolean:

(* "the account is active" *)
s.status = Active
 
(* "the cart has items" *)
s.item_count > 0
 
(* "the balance is positive" *)
s.balance > 0

State predicates appear in the given clause of scenarios — they describe preconditions that must hold before an action arrives.

Action predicates

An action predicate classifies the incoming action, optionally in terms of the current state. It receives both s : state and a : action implicitly:

(* "the operation is a deposit" *)
a.op = Deposit
 
(* "the quantity exceeds the limit" *)
a.qty > 10000
 
(* "the withdrawal amount is within the balance" *)
a.amount <= s.balance

Action predicates appear in the when clause of scenarios — they describe conditions on the action that triggers a behavior.

Note that action predicates can reference both a and s. This is important for predicates like has_sufficient_funds where the condition depends on the relationship between the action and the current state.

What predicates look like

A predicate is just a name and an IML boolean expression. The expression uses fields from s (for state predicates) or s and a (for action predicates):

The IML body is a single expression — no let bindings, no function definitions. Just a boolean condition over the state and/or action fields.

Complementary pairs

When a boundary matters, define both sides explicitly:

(* the boundary: qty = 10000 *)
qty_ok      : a.qty <= 10000
qty_too_big : a.qty > 10000

(* the boundary: amount vs balance *)
has_sufficient_funds : a.amount <= s.balance
insufficient_funds   : a.amount > s.balance

This makes scenarios precise. Instead of a single predicate that some scenarios negate implicitly, you get two named predicates that partition the space. This also helps ImandraX compute clean complement regions — the reasoning engine can see exactly which side of a boundary each scenario covers.

Where predicates come from

Predicates are derived from evidence — the concrete artifacts that ground your model:

You don't invent predicates in the abstract. You read code, tests, logs, and docs, then extract the conditions that drive branching behavior.

Predicates are reusable

Once defined, a predicate can appear in any number of scenarios:

• is_active might appear in the given of deposit_when_active, withdraw_sufficient, freeze_account, and cancel_cart
• is_deposit might appear in the when of both deposit_when_active and blocked_when_frozen

This reuse is a key property. You build a vocabulary of named conditions, then compose scenarios from that vocabulary. When a predicate changes (say, the limit moves from 10,000 to 50,000), every scenario that references it automatically reflects the new boundary.

What the reasoning engine checks

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

• Does the expression parse as valid IML?
• Do the referenced fields exist in the domain base types?
• Are the types correct? (e.g., comparing an int to an int, not an int to a variant constructor)

Each predicate is checked independently against the domain base. If validation fails, the predicate is marked invalid and any scenario that references it cannot be fully analyzed until the predicate is fixed.

See Consistency checking for more on how predicates are validated.