Example: Boundary conflict

This example demonstrates how SpecLogician detects conflicting requirements at a boundary condition and guides you toward a resolution by refining predicates.

The problem

Two requirements disagree at the boundary:

Requirement A (strict): "Reject if qty ≥ 10,000"
Requirement B (lenient): "Accept if qty ≤ 10,000"

The implementation uses <=, suggesting it accepts at equality. But the requirements overlap at qty = 10,000 — one says reject, the other says accept.

Domain base

The same small base as the order-limits example:

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

Predicates

The initial predicates follow the requirements literally:

Name	IML body	Source
`qty_ge_max`	`a.qty >= 10000`	From Requirement A
`qty_le_max`	`a.qty <= 10000`	From Requirement B

These predicates overlap at qty = 10000 — both are true simultaneously.

Transition

A single transition that implements the strict interpretation:

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

Scenarios

Scenario	When	Then	Source
`req_a_reject_ge`	`qty_ge_max`	`on_order`	Requirement A
`req_b_accept_le`	`qty_le_max`	`on_order`	Requirement B

What SpecLogician detects

When these scenarios are analyzed, ImandraX finds a scenario overlap: both req_a_reject_ge and req_b_accept_le can fire when qty = 10000. The witness is a concrete example:

qty = 10000 satisfies both a.qty >= 10000 and a.qty <= 10000

This overlap means the model is ambiguous at the boundary — two scenarios claim to handle the same input, potentially with different intentions (one expects rejection, the other acceptance).

Resolution: split the boundary

To resolve the conflict, refine the predicates by splitting the equality case:

Name	IML body	Purpose
`qty_eq_max`	`a.qty = 10000`	Exactly at the boundary
`qty_gt_max`	`a.qty > 10000`	Strictly above (always reject)
`qty_lt_max`	`a.qty < 10000`	Strictly below (always accept)

With these three predicates, you can create three non-overlapping scenarios that handle every case unambiguously. The equality case (qty = 10000) gets its own scenario where you make an explicit design decision: accept or reject.

Key takeaway

SpecLogician doesn't just flag the overlap — it provides a witness showing exactly where the conflict occurs. This turns a vague "the requirements disagree somewhere" into a precise "at qty = 10,000, both scenarios fire." The resolution pattern — splitting predicates at the boundary — is a common technique for turning ambiguous specs into precise ones.

Building this model with the CLI

Define the conflicting model

# Domain base
speclogician ch base-edit --src "type state = { pos : int; rejected : int }
type action = { qty : int }" --json
 
# Overlapping predicates (intentionally conflicting)
speclogician ch pred-add --pred-type action --pred-name qty_ge_max \
  --pred-src "a.qty >= 10000" --json
speclogician ch pred-add --pred-type action --pred-name qty_le_max \
  --pred-src "a.qty <= 10000" --json
 
# Transition
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
 
# Scenarios
speclogician ch scenario-add req_a_reject_ge \
  --when qty_ge_max --then on_order --initial --json
speclogician ch scenario-add req_b_accept_le \
  --when qty_le_max --then on_order --json

Detect the conflict

speclogician view state --compact

ImandraX will report a scenario overlap at qty = 10000.

Resolve with refined predicates

# Remove overlapping predicates and add non-overlapping ones
speclogician ch pred-remove --pred-name qty_ge_max --json
speclogician ch pred-remove --pred-name qty_le_max --json
 
speclogician ch pred-add --pred-type action --pred-name qty_eq_max \
  --pred-src "a.qty = 10000" --json
speclogician ch pred-add --pred-type action --pred-name qty_gt_max \
  --pred-src "a.qty > 10000" --json
speclogician ch pred-add --pred-type action --pred-name qty_lt_max \
  --pred-src "a.qty < 10000" --json

Using batch instead

[
  {
    "kind": "DomainModelBaseEdit",
    "new_base_src": "type state = { pos : int; rejected : int }\ntype action = { qty : int }"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "qty_ge_max",
    "pred_src": "a.qty >= 10000"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "qty_le_max",
    "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": "req_a_reject_ge",
    "when": { "add": ["qty_ge_max"] },
    "then": { "add": ["on_order"] },
    "is_initial": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "req_b_accept_le",
    "when": { "add": ["qty_le_max"] },
    "then": { "add": ["on_order"] }
  }
]

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