Example: Order limits

This example formalizes a simple rule: "Orders must be rejected if quantity exceeds the maximum order size (10,000)".

The system

  • Orders arrive with a quantity field
  • If the quantity exceeds 10,000, the order is rejected
  • Otherwise, the order is accepted and the position increases by the order quantity

Evidence

Before modeling, collect artifacts that ground the rule:

  • Requirements doc: "Order must be rejected if quantity exceeds max order size. max_qty=10000."

  • Source code (Python):

    MAX_QTY = 10_000
 
def check_qty(order) -> bool:
    return order.qty <= MAX_QTY

  • Test trace: given { pos = 0; rejected = 0 }, when { qty = 10001 }, then { pos = 0; rejected = 1 }

  • Production log: FIX message showing MaxQtyExceeded for qty=10001

Domain base

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

Design notes:

  • pos tracks the accepted position — shows that acceptance has an observable effect on state.
  • rejected counts rejections — confirms that rejection is also observable.
  • action.qty is the key input driving the rule.

Predicates

Action predicates

NameIML bodyMeaning
qty_oka.qty <= 10000Quantity is within the limit
qty_too_biga.qty > 10000Quantity exceeds the limit

These form a complementary pair — every possible quantity satisfies exactly one.

Transition

on_new_order

if a.qty > 10000 then { pos = s.pos; rejected = s.rejected + 1 }
else { pos = s.pos + a.qty; rejected = s.rejected }

A single transition handles both branches: rejection increments the counter, acceptance adds to position.

Scenarios

ScenarioWhenThenFlags
reject_on_large_qtyqty_too_bigon_new_orderinitial
accept_on_small_qtyqty_okon_new_order

Notes:

  • reject_on_large_qty is marked initial — the system starts ready to process orders.
  • No state predicates are needed because the transition logic depends only on the action.

Complement analysis

With two complementary predicates, every quantity value is covered:

  • qty <= 10000 → accepted
  • qty > 10000 → rejected

The complement may surface edge cases like qty = 0 or negative quantities — whether these should be handled differently is a design decision the model surfaces but doesn't impose.

Building this model with the CLI

Collect evidence

# Requirement from docs
speclogician ch data doc-add --art-id doc-001 \
  --text "Order must be rejected if quantity exceeds max order size. max_qty=10000." \
  --meta "From requirements.md" --json
 
# Source code
speclogician ch data src-add --art-id src-001 \
  --src-code "MAX_QTY = 10_000
 
def check_qty(order) -> bool:
    return order.qty <= MAX_QTY" \
  --language python --file-path "risk/checks/order_limits.py" --json
 
# Test trace
speclogician ch trace test-add --art-id test-001 \
  --name "Order is rejected when qty exceeds max" \
  --filepath "tests/risk/OrderValidationSpec.groovy" \
  --language groovy \
  --given "{ pos = 0; rejected = 0 }" \
  --when "{ qty = 10001 }" \
  --then "{ pos = 0; rejected = 1 }" --json
 
# Production log trace
speclogician ch trace log-add --art-id log-001 \
  --filename "prod_2026-01-09_FIX.log" \
  --contents "8=FIX.4.4|35=D|11=abc123|38=10001|55=IBM|54=1|58=MaxQtyExceeded" \
  --given "{ pos = 0; rejected = 0 }" \
  --when "{ qty = 10001 }" \
  --then "{ pos = 0; rejected = 1 }" --json

Define the model

# Domain base
speclogician ch base-edit --src "type state = { pos : int; rejected : int }
type action = { qty : int }" --json
 
# Predicates
speclogician ch pred-add --pred-type action --pred-name qty_ok \
  --pred-src "a.qty <= 10000" --json
speclogician ch pred-add --pred-type action --pred-name qty_too_big \
  --pred-src "a.qty > 10000" --json
 
# Transition
speclogician ch trans-add --trans-name on_new_order --trans-src \
  "if a.qty > 10000 then { pos = s.pos; rejected = s.rejected + 1 }
   else { pos = s.pos + a.qty; rejected = s.rejected }" --json
 
# Scenarios
speclogician ch scenario-add reject_on_large_qty \
  --when qty_too_big --then on_new_order --initial --json
speclogician ch scenario-add accept_on_small_qty \
  --when qty_ok --then on_new_order --json

Inspect and verify

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

Expected result:

  • Base status: valid
  • 2 predicates, both logic-valid
  • 1 transition, logic-valid
  • 2 scenarios, no missing components, no inconsistencies
  • Reachability: all scenarios reachable from initial
  • Complement: shows uncovered regions (e.g., if you later need to handle qty = 0 differently)
speclogician ch data link --art-id doc-001 --comp-name qty_too_big --json
speclogician ch data link --art-id src-001 --comp-name qty_ok --json
speclogician ch data link --art-id src-001 --comp-name on_new_order --json

Using batch instead

All of the above can be done in a single batch call:

[
  {
    "kind": "AddDocRef",
    "art_id": "doc-001",
    "text": "Order must be rejected if quantity exceeds max order size. max_qty=10000."
  },
  {
    "kind": "AddSrcCodeRef",
    "art_id": "src-001",
    "src_code": "MAX_QTY = 10_000\n\ndef check_qty(order) -> bool:\n    return order.qty <= MAX_QTY",
    "language": "python",
    "file_path": "risk/checks/order_limits.py"
  },
  {
    "kind": "AddTestTrace",
    "art_id": "test-001",
    "name": "Order is rejected when qty exceeds max",
    "given": "{ pos = 0; rejected = 0 }",
    "when": "{ qty = 10001 }",
    "then": "{ pos = 0; rejected = 1 }"
  },
  {
    "kind": "DomainModelBaseEdit",
    "new_base_src": "type state = { pos : int; rejected : int }\ntype action = { qty : int }"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "qty_ok",
    "pred_src": "a.qty <= 10000"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "qty_too_big",
    "pred_src": "a.qty > 10000"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "on_new_order",
    "trans_src": "if a.qty > 10000 then { pos = s.pos; rejected = s.rejected + 1 } else { pos = s.pos + a.qty; rejected = s.rejected }"
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "reject_on_large_qty",
    "when": { "add": ["qty_too_big"] },
    "then": { "add": ["on_new_order"] },
    "is_initial": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "accept_on_small_qty",
    "when": { "add": ["qty_ok"] },
    "then": { "add": ["on_new_order"] }
  }
]
speclogician ch batch --file changes.json --json
Previous← Examples
NextExample: Bank account →