Example: Traffic light

This example models a simple traffic light controller — domain types, predicates, transitions, and scenarios explained step by step.

The system

A traffic light cycles through three phases: Red, Green, and Yellow. The allowed transitions are:

Red → Green
Green → Yellow
Yellow → Red

Additionally, an emergency signal can force the light to Red from any phase.

Domain base

The domain base defines the shape of your state and actions using IML types.

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

Design notes:

phase is a variant type — this is preferred over encoding phases as integers (0, 1, 2). Variants are self-documenting and prevent meaningless values.
signal captures the two kinds of input: the normal cycle advance and an emergency override.
Both state and action are records. Even with a single field, records are extensible — you can add fields later without rewriting everything.

Predicates

Predicates are boolean classifications. They answer "what is true?" about a state or action — they don't define behavior.

State predicates

Each classifies the current phase:

Name	IML body	Meaning
`is_red`	`s.phase = Red`	Light is currently red
`is_green`	`s.phase = Green`	Light is currently green
`is_yellow`	`s.phase = Yellow`	Light is currently yellow

Action predicates

Each classifies the incoming signal:

Name	IML body	Meaning
`is_advance`	`a.signal = Advance`	Normal cycle signal
`is_emergency`	`a.signal = Emergency`	Emergency override signal

Why these predicates? Each one corresponds to a condition you'd test in a real implementation. Together they partition the input space — every combination of state and action is classifiable.

Transitions

Transitions are pure functions (state, action) → state. They define how state evolves. Every field of the state record must be assigned in the result.

`advance_from_red`

{ phase = Green }

When the light is red and receives an advance signal, it turns green.

`advance_from_yellow`

{ phase = Red }

Yellow advances to red, completing the cycle.

`go_to_red`

{ phase = Red }

Emergency signal forces the light to red regardless of current phase.

Scenarios

Each scenario captures one behavioral path through the system using given / when / then:

given — state predicates that must hold before the action
when — action predicates that classify the incoming action
then — the transition that fires

Normal cycle

Scenario	Given	When	Then	Flags
`red_to_green`	`is_red`	`is_advance`	`advance_from_red`	`initial`
`green_to_yellow`	`is_green`	`is_advance`	`advance_from_green`
`yellow_to_red`	`is_yellow`	`is_advance`	`advance_from_yellow`

The initial flag on red_to_green marks it as a reachability root — the system starts in red.

Emergency override

Scenario	Given	When	Then
`emergency_from_green`	`is_green`	`is_emergency`	`go_to_red`
`emergency_from_yellow`	`is_yellow`	`is_emergency`	`go_to_red`

No emergency_from_red scenario is needed — the light is already red.

How the pieces connect

The full model forms a cycle with an emergency shortcut:

    ┌─────────────────────────────────┐
    │                                 │
    ▼                                 │
  [Red] ──advance──▶ [Green] ──advance──▶ [Yellow]
                       │                    │
                       │ emergency           │ emergency
                       ▼                    ▼
                     [Red] ◀──advance──── [Red]

Reachability: Starting from red_to_green (initial), every scenario is reachable:

red_to_green → green_to_yellow → yellow_to_red → back to red_to_green
From green or yellow, the emergency scenarios are also reachable

Complement: With these 5 scenarios, the only uncovered region is is_red + is_emergency — which is intentionally a no-op (already red). You could add a noop scenario for completeness or leave the complement as documented behavior.

What you'd check

Once this model is loaded into SpecLogician, the reasoning engine (ImandraX) would verify:

All IML is valid — types, predicates, and transitions compile
No scenario is inconsistent — the given/when/then predicates don't contradict each other
All scenarios are reachable — every scenario can be reached from the initial
Goals and safety — if you mark scenarios as --goal or --bad, ImandraX checks liveness and safety properties
Complement regions — what behaviors are not covered by any scenario

Building this model with the CLI

Define the model

# Domain base
speclogician ch base-edit --src "type phase = Red | Green | Yellow
type signal = Advance | Emergency
type state = { phase : phase }
type action = { signal : signal }" --json
 
# State predicates
speclogician ch pred-add --pred-type state --pred-name is_red \
  --pred-src "s.phase = Red" --json
speclogician ch pred-add --pred-type state --pred-name is_green \
  --pred-src "s.phase = Green" --json
speclogician ch pred-add --pred-type state --pred-name is_yellow \
  --pred-src "s.phase = Yellow" --json
 
# Action predicates
speclogician ch pred-add --pred-type action --pred-name is_advance \
  --pred-src "a.signal = Advance" --json
speclogician ch pred-add --pred-type action --pred-name is_emergency \
  --pred-src "a.signal = Emergency" --json
 
# Transitions
speclogician ch trans-add --trans-name advance_from_red \
  --trans-src "{ phase = Green }" --json
speclogician ch trans-add --trans-name advance_from_green \
  --trans-src "{ phase = Yellow }" --json
speclogician ch trans-add --trans-name advance_from_yellow \
  --trans-src "{ phase = Red }" --json
speclogician ch trans-add --trans-name go_to_red \
  --trans-src "{ phase = Red }" --json
 
# Normal cycle scenarios
speclogician ch scenario-add red_to_green \
  --given is_red --when is_advance --then advance_from_red --initial --json
speclogician ch scenario-add green_to_yellow \
  --given is_green --when is_advance --then advance_from_green --json
speclogician ch scenario-add yellow_to_red \
  --given is_yellow --when is_advance --then advance_from_yellow --json
 
# Emergency override scenarios
speclogician ch scenario-add emergency_from_green \
  --given is_green --when is_emergency --then go_to_red --json
speclogician ch scenario-add emergency_from_yellow \
  --given is_yellow --when is_emergency --then go_to_red --json

Inspect and verify

speclogician view state --compact
speclogician reach summary --json

Using batch instead

[
  {
    "kind": "DomainModelBaseEdit",
    "new_base_src": "type phase = Red | Green | Yellow\ntype signal = Advance | Emergency\ntype state = { phase : phase }\ntype action = { signal : signal }"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "is_red",
    "pred_src": "s.phase = Red"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "is_green",
    "pred_src": "s.phase = Green"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "is_yellow",
    "pred_src": "s.phase = Yellow"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_advance",
    "pred_src": "a.signal = Advance"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_emergency",
    "pred_src": "a.signal = Emergency"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "advance_from_red",
    "trans_src": "{ phase = Green }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "advance_from_green",
    "trans_src": "{ phase = Yellow }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "advance_from_yellow",
    "trans_src": "{ phase = Red }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "go_to_red",
    "trans_src": "{ phase = Red }"
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "red_to_green",
    "given": { "add": ["is_red"] },
    "when": { "add": ["is_advance"] },
    "then": { "add": ["advance_from_red"] },
    "is_initial": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "green_to_yellow",
    "given": { "add": ["is_green"] },
    "when": { "add": ["is_advance"] },
    "then": { "add": ["advance_from_green"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "yellow_to_red",
    "given": { "add": ["is_yellow"] },
    "when": { "add": ["is_advance"] },
    "then": { "add": ["advance_from_yellow"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "emergency_from_green",
    "given": { "add": ["is_green"] },
    "when": { "add": ["is_emergency"] },
    "then": { "add": ["go_to_red"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "emergency_from_yellow",
    "given": { "add": ["is_yellow"] },
    "when": { "add": ["is_emergency"] },
    "then": { "add": ["go_to_red"] }
  }
]

speclogician ch batch --file changes.json --json