Example: Trace-driven modeling

This example demonstrates a different starting point: instead of beginning with requirements or code, you start from concrete traces — test results and production logs — and incrementally build the formal model around them.

The approach

Most examples start with a known rule and formalize it. In trace-driven modeling, you start with observed behavior and work backward:

Define the base types (minimal, just enough to express the traces)
Add test traces and log traces as artifacts
Extract predicates from the trace values
Lift traces into symbolic scenarios
Hypothesize a transition that explains all scenarios

Domain base

Start with types just large enough to express the traces:

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

Traces first

Test traces

Two test traces provide the behavioral evidence:

Accept trace:

name:  "accept_small_qty"
given: { pos = 0; rejected = 0 }
when:  { qty = 5 }
then:  { pos = 5; rejected = 0 }

Reject trace:

name:  "reject_large_qty"
given: { pos = 0; rejected = 0 }
when:  { qty = 10001 }
then:  { pos = 0; rejected = 1 }

Production log trace

filename: "prod.log"
given:    { pos = 20; rejected = 2 }
when:     { qty = 20000 }
then:     { pos = 20; rejected = 3 }
contents: "REJECT reason=MaxQtyExceeded qty=20000"

The log confirms the rejection behavior with a different starting state (pos=20, rejected=2) and provides a human-readable reason: MaxQtyExceeded.

Extracting predicates

From the traces, two boundaries emerge:

Name	IML body	Derived from
`qty_small`	`a.qty <= 10`	Accept trace used qty=5
`qty_huge`	`a.qty > 10000`	Reject traces used qty=10001 and qty=20000

Note that these predicates don't cover the full space — quantities between 11 and 10,000 are unclassified. This is intentional at this stage — the complement will surface this gap.

Scenarios (without transitions)

Initially, scenarios are created with only when clauses — no transitions yet:

Scenario	When	Then	Notes
`accept_small`	`qty_small`	(empty)	Lifted from accept trace
`reject_huge`	`qty_huge`	(empty)	Lifted from reject traces

These scenarios are marked Missing because they lack transitions. But they capture the behavioral intent: small quantities are accepted, huge quantities are rejected.

Adding a transition

Once the pattern is clear, hypothesize a transition:

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

This single transition explains both the accept and reject traces. Adding it to the scenarios' then clauses completes them.

What the complement reveals

With two predicates (qty_small ≤ 10 and qty_huge > 10000), the complement shows:

11 ≤ qty ≤ 10000 — a large gap with no scenario. Are these accepted? Rejected? The traces don't say.

This gap drives the next iteration: add a predicate for the middle range and a corresponding scenario:

qty_mid : a.qty > 10 && a.qty <= 10000

Trace matching

Once scenarios have complete predicates and transitions, ImandraX can match the traces:

Accept trace (qty = 5) matches accept_small — satisfies qty_small, and applying on_order produces the expected then-state
Reject traces (qty = 10001, qty = 20000) match reject_huge — satisfy qty_huge, and on_order produces the expected then-states

Unmatched traces would indicate scenarios that need adjustment or new scenarios that need to be created.

Key takeaway

Trace-driven modeling inverts the usual workflow. Instead of "write the spec, then check against tests," you start with "here's what the system actually does" and build the spec around the evidence. The complement guides you toward completeness, and trace matching validates that the formal model is consistent with the observed behavior.

This approach works well when:

You have a legacy system with tests but no formal requirements
You're investigating production incidents and want to understand behavior boundaries
You're building a model for an existing codebase and want the spec grounded in real data from the start

Building this model with the CLI

Start with traces

# Domain base
speclogician ch base-edit --src "type state = { pos : int; rejected : int }
type action = { qty : int }" --json
 
# Test traces
speclogician ch trace test-add --art-id test-001 \
  --name "accept_small_qty" \
  --given "{ pos = 0; rejected = 0 }" \
  --when "{ qty = 5 }" \
  --then "{ pos = 5; rejected = 0 }" --json
 
speclogician ch trace test-add --art-id test-002 \
  --name "reject_large_qty" \
  --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.log" \
  --contents "REJECT reason=MaxQtyExceeded qty=20000" \
  --given "{ pos = 20; rejected = 2 }" \
  --when "{ qty = 20000 }" \
  --then "{ pos = 20; rejected = 3 }" --json

Extract predicates and build the model

# Predicates derived from trace values
speclogician ch pred-add --pred-type action --pred-name qty_small \
  --pred-src "a.qty <= 10" --json
speclogician ch pred-add --pred-type action --pred-name qty_huge \
  --pred-src "a.qty > 10000" --json
 
# Scenarios (initially without transitions)
speclogician ch scenario-add accept_small \
  --when qty_small --initial --json
speclogician ch scenario-add reject_huge \
  --when qty_huge --json
 
# Add a transition once the pattern is clear
speclogician ch trans-add --trans-name on_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
 
# Update scenarios with the transition
speclogician ch scenario-edit accept_small --then on_order --json
speclogician ch scenario-edit reject_huge --then on_order --json

Inspect and verify

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

Using batch instead

[
  {
    "kind": "DomainModelBaseEdit",
    "new_base_src": "type state = { pos : int; rejected : int }\ntype action = { qty : int }"
  },
  {
    "kind": "AddTestTrace",
    "art_id": "test-001",
    "name": "accept_small_qty",
    "given": "{ pos = 0; rejected = 0 }",
    "when": "{ qty = 5 }",
    "then": "{ pos = 5; rejected = 0 }"
  },
  {
    "kind": "AddTestTrace",
    "art_id": "test-002",
    "name": "reject_large_qty",
    "given": "{ pos = 0; rejected = 0 }",
    "when": "{ qty = 10001 }",
    "then": "{ pos = 0; rejected = 1 }"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "qty_small",
    "pred_src": "a.qty <= 10"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "qty_huge",
    "pred_src": "a.qty > 10000"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "on_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": "accept_small",
    "when": { "add": ["qty_small"] },
    "then": { "add": ["on_order"] },
    "is_initial": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "reject_huge",
    "when": { "add": ["qty_huge"] },
    "then": { "add": ["on_order"] }
  }
]

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