State instances and diffs
SpecLogician tracks model evolution through immutable state instances. Every change — adding a predicate, editing a transition, removing a scenario — produces a new snapshot. The difference between consecutive snapshots is a diff that makes progress visible and measurable.
State instances
A state instance is a complete, immutable snapshot of the model at a point in time. It contains:
- The Spec — domain base, predicates, transitions, scenarios, plus all analysis results (validity, conflicts, complement, reachability)
- The artifact container — test traces, log traces, doc refs, source code refs, and artifact-to-component mappings
When a change is applied:
- The change modifies the current Spec and/or artifact container
- ImandraX analyzes the affected components (only what changed — not the whole model)
- A new immutable state instance is created from the results
- A diff is computed between the old and new instances
This makes iteration safe for agentic workflows. An LLM can propose a change, inspect the diff to see if it improved or regressed, and undo if needed — all through structured, machine-readable operations.
What diffs measure
A diff captures every dimension of change between two state instances. Each metric has an outcome: IMPROVED, DECLINED, NO_CHANGE, or UNKNOWN.
Component counts
Basic structural changes:
- Number of state predicates, action predicates, transitions, scenarios
- Number added, removed, or modified
Validity
How many components pass IML validation:
- Predicates with valid IML (before vs after)
- Transitions with valid IML
- Scenarios with valid component references (no missing predicates/transitions)
Consistency
Logical soundness of the model:
- Number of scenarios with satisfiable predicate conjunctions
- Number of inconsistent scenarios (contradictory predicates)
- Number of scenario conflicts (overlaps and consumed relationships)
Coverage
How much of the behavior space is specified:
- Number of complement regions (uncovered state/action combinations)
- Regions added vs removed between instances
Reachability
How well-connected the scenario graph is:
- Number of reachable scenarios (from initials)
- Number of unreachable scenarios
- Safety violations (reachable bad scenarios)
- Liveness violations (unreachable goal scenarios)
Artifact linking
How well the formal model is grounded in evidence:
- Number of components linked to at least one artifact
- Number of matched vs unmatched traces
Progress metrics
Every diff includes a progress section with five quantified optimization targets:
| Metric | Meaning | Target |
|---|---|---|
scenarios_valid_pct | % of scenarios with no missing or inconsistent components | 100.0 |
reachability_pct | % of scenarios reachable from initial states | 100.0 |
components_valid_pct | % of predicates + transitions with valid IML | 100.0 |
linked_artifacts_pct | % of components linked to at least one artifact | 100.0 |
complement_regions | Number of uncovered behavior regions | 0 |
These metrics give you a single dashboard for spec maturity. In an agentic workflow, an LLM can read these values after each change and decide what to work on next: fix invalid IML, add scenarios to cover complement gaps, or link artifacts to components.
Values are null when the denominator is zero (e.g., no scenarios exist yet).
Undo
If a change makes things worse — more inconsistencies, new complement regions, broken validity — you can roll it back:
Undone instances are moved to an internal stash, not lost. The state file is updated immediately. This is particularly useful in agentic workflows where an LLM might make speculative changes that need to be reversed.
The change pipeline
Every change flows through the same pipeline:
Parse → Apply → Analyze → Diff → Save
- Parse — the change (JSON or CLI arguments) is deserialized into a typed StateChange
- Apply — the change modifies the current Spec or artifact container
- Analyze — ImandraX checks affected components (scoped to what changed)
- Diff — before/after metrics are compared, outcomes assigned
- Save — the new state instance is persisted to disk
The analysis step is incremental. A predicate edit only rechecks that predicate plus any scenarios that reference it. A scenario removal triggers a broader refresh (checking for orphaned components). A domain base edit rechecks everything, since all components depend on the base types.
Recommendations
After computing a diff, SpecLogician generates recommendations — ranked, actionable suggestions for what to do next. These are derived from the current state and the diff:
- If predicates have invalid IML → fix the syntax errors first (blocks downstream analysis)
- If scenarios reference undefined predicates → add the missing predicates
- If scenarios are inconsistent → relax contradictory predicate conjunctions
- If complement regions exist → add scenarios to cover the gaps
- If traces are unmatched → adjust predicates or add scenarios to match them
- If artifacts exist but aren't linked → run trace matching
Recommendations close the feedback loop. After each change, the model tells you what needs attention next.