State and action

The domain base is the foundation of every SpecLogician model. It defines two types in IML (Imandra Modeling Language): what a state looks like and what an action looks like. Everything else — predicates, transitions, scenarios — is written in terms of these types.

The two required types

Every domain base must define a state type and an action type.

state represents the system's current condition — the things that persist between actions:

type state = { balance : int; status : account_status }

action represents an input or event that arrives and may change the state:

type action = { op : op_kind; amount : int }

Both are IML record types — named collections of typed fields.

IML type system

IML supports three type constructs relevant to modeling:

Records

The primary way to define state and action. Each field has a name and a type:

type state = { balance : int; frozen : int }
type action = { qty : int }

Fields can be int (integers), other record types, or variant types.

Variant types

Algebraic data types that enumerate a fixed set of alternatives:

type op_kind = Deposit | Withdraw | Freeze | Unfreeze
type phase = Init | Authed | Ready
type account_status = Active | Frozen | Closed

Each constructor is a distinct, named value. There are no "invalid" values — every instance of op_kind is exactly one of the four constructors.

Nested records

For larger systems, compose state from sub-records:

type auth_info = { role : role_kind; logged_in : int }
type billing_info = { balance : int; frozen : int }
type state = { auth : auth_info; billing : billing_info }

This keeps the top-level state organized as the model grows. Predicates and transitions access nested fields with dot notation: s.billing.balance.

Why variants over integers

Always prefer variant types over integer encodings for categorical values.

Reserve int for genuine numeric values: quantities, balances, counters, timestamps. Use variants for anything that represents a category, phase, mode, or operation kind.

This matters especially for complement analysis — when SpecLogician computes the state/action space not covered by your scenarios, integer-encoded categories create spurious "gap" regions that don't correspond to real behaviors.

Designing a good domain base

The domain base should be the smallest set of types that can express all the behaviors you care about. Some guidelines:

• Start small. You can always add fields later. Begin with just the fields needed by your first few scenarios.
• Model observable effects. If an action changes something (a counter increments, a status flips, a balance moves), that something should be a field in state.
• Model decision inputs. If the system's behavior depends on an input value (a quantity, an operation type, a flag), that value should be a field in action.
• Don't model implementation details. The domain base captures what the system tracks, not how it's implemented. You don't need database schemas, network protocols, or class hierarchies.

Example: Order validation

The rule is "reject orders with quantity > 10,000". What do we need?

• The action carries a quantity → action.qty : int
• The system tracks position and rejection count → state.pos : int; state.rejected : int

type state = { pos : int; rejected : int }
type action = { qty : int }

Two types, three fields. Enough to express accept/reject behavior, position changes, and rejection counting.

Example: Traffic light

The system cycles through phases and responds to signals:

type phase = Red | Green | Yellow
type signal = Advance | Emergency
type state = { phase : phase }
type action = { signal : signal }

Variant types make the domain precise — there's no phase = 4 to worry about.

Evolving the base

The domain base isn't frozen after the first edit. As you formalize more behaviors, you'll add fields:

(* started with *)
type state = { balance : int }
 
(* later expanded to *)
type state = { balance : int; status : account_status; audit_count : int }

Existing predicates and transitions that reference unchanged fields continue to work. Predicates and transitions that reference new fields will need to be added or updated — SpecLogician's analysis will flag any that become invalid after a base change.