Example: Risk flag latch

This example models a latched risk flag — once raised, it blocks all new orders until explicitly reset. It demonstrates stateful guards, reset transitions, and reachability through a mandatory intermediate step.

The rule

If a risk flag is raised, all new orders are rejected until a reset occurs.

This is a latch: once activated, it stays active until explicitly cleared. Orders can only be accepted again after the reset.

Domain base

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

risk_active is a boolean latch — true means all orders are blocked
kind encodes the action type (0 = NewOrder, 1 = Reset)
pos tracks accepted position, rejected counts rejections

Predicates

State predicates

Name	IML body	Meaning
`risk_on`	`s.risk_active = true`	Risk flag is active — orders blocked
`risk_off`	`s.risk_active = false`	Risk flag is clear — orders accepted

Action predicates

Name	IML body	Meaning
`is_order`	`a.kind = 0`	Incoming new order
`is_reset`	`a.kind = 1`	Reset signal

Transition

A single transition handles all three branches:

(* step *)
if a.kind = 1 then
  { pos = s.pos; rejected = s.rejected; risk_active = false }
else if s.risk_active then
  { pos = s.pos; rejected = s.rejected + 1; risk_active = true }
else
  { pos = s.pos + a.qty; rejected = s.rejected; risk_active = false }

Reset → clears the flag
Order while risk is on → rejected, flag stays on
Order while risk is off → accepted, position increases

Scenarios

Scenario	Given	When	Then	Meaning
`reject_when_risk_on`	`risk_on`	`is_order`	`step`	Order blocked by active risk flag
`accept_when_risk_off`	`risk_off`	`is_order`	`step`	Normal order acceptance
`reset_clears_risk`	`risk_on`	`is_reset`	`step`	Reset clears the latch

Reachability

The reachability graph tells the story of the latch lifecycle:

[accept_when_risk_off] ←──── [reset_clears_risk]
                                      ↑
                              [reject_when_risk_on]
                                      ↑
                                (risk event)

Starting from accept_when_risk_off:

After a risk event raises the flag (not modeled — would need a raise_risk scenario), orders are rejected
The only path back to acceptance is through reset_clears_risk
reset_clears_risk is the mandatory intermediate step between rejection and acceptance

Complement gaps

The complement reveals:

risk_off + is_reset — what happens if reset is called when the flag is already clear? The transition handles it (no-op), but there's no explicit scenario.
Missing risk-raise scenario — there's no scenario for how the flag gets set to true in the first place. The model currently starts from either state but doesn't model the transition between them.

These gaps guide the next iteration: add a raise_risk scenario and a reset_when_clear no-op.

Evidence grounding

This demo includes concrete artifacts that ground the model:

Requirements excerpt: "risk flag blocks trading"
Source code: Python implementation showing the on_new_order, on_risk_event, and on_reset handlers
Test trace: latch raised → order rejected → reset → order accepted
Production log: REJECT reason=RiskFlagActive qty=1 confirming real-world behavior

The test trace matches reject_when_risk_on (the order-rejected step), and the log trace provides production evidence for the same rejection path.

Key takeaway

The latch pattern is common in risk management, safety systems, and protocol design. SpecLogician's reachability analysis formally proves that the only path from rejection back to acceptance is through reset — a critical safety property. The complement identifies edge cases (reset when already clear, how the flag gets raised) that the model should address.

Building this model with the CLI

Collect evidence

speclogician ch data doc-add --art-id doc-001 \
  --text "If a risk flag is raised, all new orders are rejected until a reset occurs." \
  --meta "Risk management requirements" --json
 
speclogician ch data src-add --art-id src-001 \
  --src-code "def on_new_order(state, order):
    if state.risk_active:
        return reject(state, order)
    return accept(state, order)
 
def on_reset(state):
    state.risk_active = False" \
  --language python --file-path "risk/handlers.py" --json

Define the model

# Domain base
speclogician ch base-edit --src "type state = { pos : int; rejected : int; risk_active : bool }
type action = { kind : int; qty : int }" --json
 
# State predicates
speclogician ch pred-add --pred-type state --pred-name risk_on \
  --pred-src "s.risk_active = true" --json
speclogician ch pred-add --pred-type state --pred-name risk_off \
  --pred-src "s.risk_active = false" --json
 
# Action predicates
speclogician ch pred-add --pred-type action --pred-name is_order \
  --pred-src "a.kind = 0" --json
speclogician ch pred-add --pred-type action --pred-name is_reset \
  --pred-src "a.kind = 1" --json
 
# Transition
speclogician ch trans-add --trans-name step --trans-src \
  "if a.kind = 1 then
    { pos = s.pos; rejected = s.rejected; risk_active = false }
   else if s.risk_active then
    { pos = s.pos; rejected = s.rejected + 1; risk_active = true }
   else
    { pos = s.pos + a.qty; rejected = s.rejected; risk_active = false }" --json
 
# Scenarios
speclogician ch scenario-add reject_when_risk_on \
  --given risk_on --when is_order --then step --json
speclogician ch scenario-add accept_when_risk_off \
  --given risk_off --when is_order --then step --initial --json
speclogician ch scenario-add reset_clears_risk \
  --given risk_on --when is_reset --then step --json

Inspect and verify

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

Using batch instead

[
  {
    "kind": "AddDocRef",
    "art_id": "doc-001",
    "text": "If a risk flag is raised, all new orders are rejected until a reset occurs."
  },
  {
    "kind": "DomainModelBaseEdit",
    "new_base_src": "type state = { pos : int; rejected : int; risk_active : bool }\ntype action = { kind : int; qty : int }"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "risk_on",
    "pred_src": "s.risk_active = true"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "risk_off",
    "pred_src": "s.risk_active = false"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_order",
    "pred_src": "a.kind = 0"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_reset",
    "pred_src": "a.kind = 1"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "step",
    "trans_src": "if a.kind = 1 then { pos = s.pos; rejected = s.rejected; risk_active = false } else if s.risk_active then { pos = s.pos; rejected = s.rejected + 1; risk_active = true } else { pos = s.pos + a.qty; rejected = s.rejected; risk_active = false }"
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "reject_when_risk_on",
    "given": { "add": ["risk_on"] },
    "when": { "add": ["is_order"] },
    "then": { "add": ["step"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "accept_when_risk_off",
    "given": { "add": ["risk_off"] },
    "when": { "add": ["is_order"] },
    "then": { "add": ["step"] },
    "is_initial": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "reset_clears_risk",
    "given": { "add": ["risk_on"] },
    "when": { "add": ["is_reset"] },
    "then": { "add": ["step"] }
  }
]

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