Scenarios
Scenarios are the core unit of formalization in SpecLogician. Instead of writing one large formal specification, you build a constellation of small, composable behavior slices — each describing one path through the system.
Anatomy of a scenario
A scenario has a name and three clauses composed from predicates and transitions:
- given — zero or more state predicates that must hold before the action
- when — zero or more action predicates that classify the incoming action
- then — one or more transitions that fire when the conditions are met
For example, a scenario withdraw_sufficient in a bank account model:
| Clause | Components | Meaning |
|---|---|---|
| given | is_active | The account is active |
| when | is_withdrawal, has_sufficient_funds | The action is a withdrawal and the balance covers it |
| then | do_withdraw | Subtract the amount from the balance |
The scenario reads as: given the account is active, when a withdrawal arrives and the balance is sufficient, then do the withdrawal.
Multiple predicates in the same clause are conjunctive — all must hold simultaneously. is_withdrawal AND has_sufficient_funds must both be true.
Why scenarios work well with LLMs
LLM-powered tools are good at:
- Proposing local behaviors ("what happens when a frozen account gets a deposit?")
- Making incremental edits (add a predicate, adjust a transition)
- Emitting structured deltas (add/remove/edit operations)
They are not good at maintaining one large, globally consistent formal artifact.
Scenarios let an LLM operate on small, self-contained targets while the reasoning engine (ImandraX) handles global consistency — checking that scenarios don't contradict each other, that they're reachable, and that together they cover the behavior space.
Scenarios partition behavior
Each scenario covers one path. Together, they describe the system. Consider a bank account with 6 scenarios:
Happy paths:
| Scenario | Given | When | Then |
|---|---|---|---|
deposit_when_active | is_active | is_deposit | do_deposit |
withdraw_sufficient | is_active | is_withdrawal, has_sufficient_funds | do_withdraw |
freeze_account | is_active | is_freeze | do_freeze |
unfreeze_account | is_frozen | is_unfreeze | do_unfreeze |
Rejection paths:
| Scenario | Given | When | Then |
|---|---|---|---|
withdraw_insufficient | is_active | is_withdrawal, insufficient_funds | noop |
blocked_when_frozen | is_frozen | is_deposit | noop |
Each scenario is small and readable on its own. The reasoning engine checks the collection as a whole — overlap detection, reachability, complement gaps.
Scenario flags
Scenarios support three boolean flags that control how the reasoning engine analyzes them:
initial
Marks a scenario as a reachability root. The system "starts here" for reachability analysis. At least one scenario should be marked initial — it seeds the BFS traversal of the reachability graph.
Typically, your initial scenario represents the entry point or default state of the system: boot, add_first_item, red_to_green.
goal
Marks a scenario as a liveness target. The reasoning engine checks that this scenario is reachable from at least one initial scenario. If it's not reachable, a liveness violation is reported.
Use goals for outcomes that must be achievable: checkout_cart, test_passes, order_accepted.
bad
Marks a scenario as a safety target. The reasoning engine checks that this scenario is not reachable from any initial scenario. If it is reachable, a safety violation is reported along with the shortest path to it.
Use bad scenarios for failure modes that should be impossible: system_panic, negative_balance, unauthorized_access.
Building scenarios incrementally
You don't need all scenarios upfront. The typical flow is:
- Start with one or two happy-path scenarios. Mark one as
initial. - Run analysis. The complement shows uncovered regions — combinations of state and action predicates that no scenario handles.
- Add scenarios to cover the gaps. Rejection paths, edge cases, error handling.
- Repeat. Each iteration adds scenarios, reduces complement regions, and improves reachability coverage.
This is the core iteration loop. The complement guides you toward completeness without requiring you to think of everything at once.
Scenarios reference, not define
Scenarios don't contain logic — they reference predicates and transitions by name. This separation is important:
- Predicates define what's true (the vocabulary)
- Transitions define what happens (the transformations)
- Scenarios compose them into behavioral paths (the grammar)
If a predicate's definition changes (say, the qty limit moves from 10,000 to 50,000), every scenario that references that predicate automatically reflects the new boundary. No scenario edits needed.
If a scenario references a predicate or transition that doesn't exist, it's marked missing and can't be fully analyzed until the missing component is defined.
What the reasoning engine checks
Scenarios are the richest analysis target. When you add, edit, or remove a scenario, ImandraX checks:
- Completeness — do all referenced predicates and transitions exist in the domain model?
- Consistency — are the given predicates mutually satisfiable? Are the when predicates satisfiable? Is the full conjunction satisfiable?
- Conflicts — do any two scenarios overlap (both could fire for the same state/action)? Does one scenario logically subsume another?
- Reachability — can every scenario be reached from an initial scenario? Are goals reachable? Are bad scenarios unreachable?
- Complement — what state/action combinations are not covered by any scenario?
See Consistency checking, Reachability, and Coverage and gaps for details on each.