Coverage and gaps

Coverage analysis answers the question: what behaviors are not specified? SpecLogician computes the complement — the set of state/action combinations that no scenario covers — and decomposes it into distinct regions. Each region represents a gap in the specification that you may want to address.

What the complement is

Given a set of scenarios, each scenario covers a region of the state/action space defined by its predicate conjunction (given + when). The complement is everything outside the union of those regions:

complement = NOT (scenario_1 OR scenario_2 OR ... OR scenario_n)

ImandraX decomposes this into a set of disjoint regions, each described by a minimal set of predicate values. These regions are the "gaps" — concrete descriptions of what the model doesn't handle.

How regions look

Each complement region is a satisfying assignment over the model's predicates. For example, in a bank account model with 6 scenarios, the complement might include:

Each region is a concrete gap that you can inspect and decide whether to cover:

• Intentional gap — the behavior is undefined by design (e.g., unfreezing an already-active account is meaningless). Document it and move on.
• Missing scenario — the behavior should be specified. Add a scenario (typically with a noop transition for rejection cases, or a real transition for valid cases).
• Missing predicate — the gap reveals a distinction you haven't modeled yet. Add a predicate to split the space.

Prerequisites for complement computation

The complement can only be computed when:

1. The domain base is valid (IML compiles)
2. At least one scenario exists and is checkable (no missing components, consistent predicates)

If these conditions aren't met, complement computation is skipped — it would be meaningless to compute gaps over an invalid or empty model.

Scenarios that are Missing or Inconsistent are excluded from the complement calculation. Only Valid scenarios contribute.

The complement drives iteration

The complement is the primary mechanism for incremental specification. The workflow is:

1. Add a few scenarios covering the obvious behaviors
2. Compute the complement — see what's not covered
3. Pick a gap, decide how to handle it
4. Add a scenario (or decide the gap is intentional)
5. Recompute — the complement shrinks

Each iteration is measurable. The complement_regions metric in the diff tells you exactly how many regions remain. The target is zero — every state/action combination is covered by some scenario.

In practice, reaching zero complement regions means you've thought about every combination of your predicates. This doesn't mean the model is complete in an absolute sense — you might need more predicates to capture finer distinctions — but it means the current vocabulary is fully utilized.

Complement and variant types

This is where variant types pay off. When categorical values are modeled as variants:

type op_kind = Deposit | Withdraw | Freeze | Unfreeze

The complement regions only contain valid constructors. Every gap corresponds to a real behavior.

When categorical values are modeled as integers:

type action = { op : int }  (* 0=Deposit, 1=Withdraw, ... *)

The complement includes regions like op = 5 or op = -1 — values that don't correspond to any real operation. These spurious regions pollute the complement and make it harder to identify genuine gaps.

Complement diff

When a change modifies scenarios, the complement is recomputed. The diff tracks:

• Regions removed — gaps that were covered by the new/modified scenario
• Regions added — new gaps introduced (this can happen if you remove a scenario or add a predicate that splits existing regions)
• Net change — the total count of complement regions before and after

A good change reduces complement regions. An unexpected increase indicates the change may have introduced a gap — check the new regions to understand why.

Example: Traffic light

A traffic light model with three normal-cycle scenarios:

The complement for these 3 scenarios includes:

Three gaps, all related to the emergency signal. Adding two emergency scenarios (from green and from yellow) reduces the complement to one region: emergency while red — which is intentionally a no-op.