Consistency checking

Consistency checking is the first line of defense. Before SpecLogician can reason about coverage, reachability, or conflicts, it needs to know that every component is well-formed and logically satisfiable. This happens at three levels: the domain base, individual components (predicates and transitions), and scenarios.

Level 1: Domain base validation

The domain base defines the state and action types that everything else builds on. When the base is added or edited, ImandraX checks:

• Syntax — does the IML parse correctly?
• Type definitions — are all types well-formed? Do variant types have valid constructors? Do records have valid field types?
• Required types — are both state and action defined?

If the base is invalid, all downstream analysis is blocked. Predicates and transitions reference base fields, so nothing can be checked until the base compiles.

The base is assigned a status: Valid, Invalid IML, or Unknown (if the check couldn't complete).

Level 2: Component validation

Each predicate and transition is validated independently against the domain base.

Predicate validation

For each predicate, ImandraX loads a minimal IML model containing just the base types and that predicate, then type-checks it:

• Do the referenced fields exist? (e.g., does s.balance exist if the state type has a balance field?)
• Are the types compatible? (e.g., comparing s.status = Active only works if status is of a variant type that includes Active)
• Is the expression a valid boolean expression?

A state predicate references s : state. An action predicate references both s : state and a : action.

Transition validation

For each transition, ImandraX checks:

• Does the expression return a value of type state?
• Are all fields of the state record assigned in the returned value?
• Are the field types correct?

Independent checking

Each component is checked in isolation — a predicate doesn't need other predicates to be valid, and a transition doesn't depend on predicates. This means:

• Invalid components don't block validation of other components
• You can fix one component at a time without cascading re-analysis
• The results tell you exactly which components have problems

Each component gets a verdict: Valid (IML compiles), Invalid (with an error message explaining why), or Unknown.

Level 3: Scenario consistency

Scenarios compose predicates and transitions by name. Their consistency is checked at multiple levels:

Completeness

Do all referenced predicates and transitions exist in the domain model?

• If a scenario references is_active but no predicate named is_active exists → the scenario is marked Missing
• Missing scenarios can't be analyzed further until the referenced components are defined

Predicate satisfiability

Even if all components exist and are individually valid, the conjunction of predicates in a scenario might be contradictory. ImandraX checks three levels of satisfiability:

Given predicates — can all state predicates in the given clause be true simultaneously?

For example, if a scenario has given: [is_active, is_frozen] and these predicates are s.status = Active and s.status = Frozen, the conjunction is unsatisfiable — a status can't be both Active and Frozen. The scenario is marked Inconsistent.

When predicates — can all action predicates in the when clause be true simultaneously?

For example, when: [is_deposit, is_withdrawal] with a.op = Deposit and a.op = Withdraw — the action can't be both. Inconsistent.

All predicates together — can the full conjunction of given + when predicates be satisfied?

This catches cross-clause contradictions. For example, given: [has_balance] with s.balance > 0 and when: [insufficient_funds] with a.amount > s.balance — these are individually satisfiable but together constrain the space. ImandraX determines whether a satisfying assignment exists.

Scenario status

After all checks, each scenario gets a component status:

Only Valid scenarios participate in downstream analysis (complement, reachability, conflict detection).

Conflict detection

Beyond individual scenario consistency, ImandraX checks for conflicts between scenarios. Two types of conflicts are detected:

Overlap

Two scenarios overlap when there exists a state/action pair that satisfies both scenarios' predicate conjunctions simultaneously.

For example, if scenario A has when: [qty_ok] (qty ≤ 10000) and scenario B has when: [qty_small] (qty ≤ 5000), then any action with qty ≤ 5000 satisfies both. ImandraX reports the overlap with a witness — a concrete state/action pair that demonstrates the conflict.

Overlaps aren't necessarily bugs. Two scenarios might intentionally cover the same region with the same transition. But they're worth reviewing — they can indicate ambiguous or redundant specification.

Consumed (subsumption)

Scenario B is consumed by scenario A when B's constraints logically imply A's — meaning every state/action pair that satisfies B also satisfies A. B is a strict special case of A.

For example, if A has when: [is_withdrawal] and B has when: [is_withdrawal, insufficient_funds], then B is consumed by A — every insufficient-funds withdrawal is also a withdrawal.

Consumed scenarios are often intentional (B adds a more specific guard to a general case), but can also indicate that a scenario is redundant.

Incremental analysis

Consistency checking is scoped to what changed:

This keeps analysis fast even as the model grows. A predicate edit doesn't recheck unrelated transitions or scenarios.