Glossary

Domain model: The shared logic layer (types, predicates, transitions).
Predicate: A boolean property over state/action. State predicates take s, action predicates take s and a.
Transition: A function describing how actions change state. Takes (s, a), returns a new state.
Scenario: A local behavior slice encoded as given/when/then. Given = state predicates, When = action predicates, Then = transitions.
State instance: An immutable snapshot of the evolving spec state after a change.
Diff: A structured summary of what changed between two instances, including progress metrics.
Artifact: Evidence/grounding (test traces, log traces, doc refs, source code refs).
Artifact map: Bidirectional links between artifacts and model components (predicates/transitions).
Complement: The set of (state, action) combinations not covered by any scenario. Fewer regions = better coverage.
Reachability graph: A graph showing which scenarios can follow which, based on transition outputs satisfying predicate inputs.
Initial scenario: A scenario marked as a root for reachability analysis.
Goal scenario: A scenario marked as a liveness target — it must be reachable from initial states. Unreachable goals indicate missing transitions or over-constrained predicates.
Bad scenario: A scenario marked as a safety target — it must NOT be reachable from initial states. Reachable bad scenarios indicate a failure mode that the system can reach (e.g., a panic, crash, or incorrect output).
Safety: A property that holds when no bad scenario is reachable from any initial. Checked with reach safety.
Liveness: A property that holds when all goal scenarios are reachable from initials. Checked with reach liveness.
Safety violation: A bad scenario that IS reachable, with a path from an initial showing how the failure occurs. This is a counterexample.
Batch: Multiple changes applied in one pass, with analysis running once at the end.
IML: Imandra Modeling Language — an ML-family language used for types, predicates, and transitions.
Progress metrics: Quantified percentages (scenarios_valid_pct, reachability_pct, components_valid_pct, linked_artifacts_pct, complement_regions) computed from the current state.