Reachability

Reachability analysis answers the question: can the system get from here to there? SpecLogician builds a directed graph whose nodes are state regions and whose edges are scenarios that move between regions, then uses it to check safety properties (bad states are unreachable), liveness properties (goal states are reachable), and overall connectivity.

The reachability graph

The reachability graph is state-centric:

• Nodes are state regions — a unique conjunction of state predicates drawn from some scenario's given, or a sink valuation reached by a scenario but not described by any scenario's preconditions.
• Edges are scenarios. A scenario whose given set defines node A and whose transition's post-state satisfies node B's given set contributes an edge A → B.

In other words: each scenario is a labeled transition between two state regions. After scenario X fires from region A, the resulting state matches region B (the most-specific observed region whose given predicates the post-state satisfies). If no observed region matches, the post-state becomes a sink.

ImandraX resolves each scenario's post-state by solving the constraints pre(s) ∧ when(s, a) ∧ post = trans(s, a) and recording a concrete witness valuation. The witness is stored on the edge.

Node kinds

Sinks are colored differently in the dashboard (a distinct copper tone) so they're visually distinct from regions that simply aren't reachable. "Reached but undefined-from" is a different failure mode than "can't be reached at all."

Flag lift

Scenario flags lift to the node kind they touch:

• --initial on a scenario marks its source node as an initial — that's where reachability BFS starts.
• --goal and --bad on a scenario mark the destination node — the region the scenario lands in.

If multiple scenarios share a given set, marking any one of them initial makes the shared node initial.

Initial scenarios

At least one scenario should be marked --initial. Initial scenarios are the roots of the reachability traversal — BFS starts from their source node and walks outgoing edges.

Typically the initial scenario represents the system's starting state: an empty cart, a fresh account, a red traffic light. Its given predicates should match the system's default values.

From the initials, SpecLogician computes:

• Reachable nodes — every state region reachable via any path from an initial node
• Unreachable scenarios — scenarios whose source node is not reachable from any initial

An unreachable scenario indicates:

• A missing intermediate scenario (the graph has a gap)
• A source region that the spec never enters
• Over-restrictive given predicates

Safety properties

A scenario marked --bad represents a failure mode — a region of state space the system should never reach. The reasoning engine checks:

Is the bad node reachable from any initial node?

• If not reachable → the property is SAFE. No sequence of scenarios from any initial can land the system in the bad region.
• If reachable → safety violation. SpecLogician reports the shortest path of state regions from an initial to the bad node, with the scenario labels on each edge.

Example

(* bad scenario: failure counter at threshold, account still unlocked *)
bad_threshold_unlocked
  given: failures_at_threshold, is_unlocked   (* s.failures = 5 ∧ ¬s.locked *)
  flag:  bad

If the lockout transition is correct, this region should be unreachable. If a buggy trans_login_fail lets failures hit 5 without setting locked = true, the path from failures_eq_0 through fail_step_1 … fail_step_5_fifth_attempt to failures_at_threshold ∧ is_unlocked becomes the reported counterexample.

Liveness properties

A scenario marked --goal represents a desired outcome — a region the system should be able to reach. The reasoning engine checks:

Is the goal node reachable from at least one initial node?

• If reachable → the property is LIVE. A path from some initial to the goal exists.
• If not reachable → liveness violation. The goal is disconnected from every initial.

Sinks and frontier gaps

A sink is a post-state valuation that some scenario lands in but no scenario's given matches. The system gets there but has nothing to say about what happens next.

The frontier consists of nodes whose only outgoing edges loop back to themselves (or none). Frontier nodes are where the reachability graph "stops" — either intentionally (terminal states) or because a successor scenario is missing.

Both are surfaced separately:

• speclogician reach frontier — lists scenarios whose post-state lands in a sink or whose successor set is only themselves
• Sinks are visually marked in the dashboard and in the node-detail panel ("No scenario in the spec uses this exact pre-state — add one to make this region observable")

Unspecified edge cases

A separate concept from sinks: an unspecified edge case is a (state, action) input region that no scenario's given ∧ when matches. The system never even enters the corresponding scenario.

• Sink = output-side gap. Reached but undefined-from.
• Unspecified edge case = input-side gap. No scenario matches this input.

Unspecified edge cases live in spec.scenario_comp.regions and are surfaced on the dashboard's Missing/Unspecified Edgecases tab, with structured constraints, an invariant, a sample model (rendered as let s = {...} / let a = {...} blocks), and cross-links to predicates and scenarios that touch the same fields. See Coverage and gaps for the complement decomposition behind them.

Trace reachability

Beyond the formal reachability graph, SpecLogician can check whether concrete traces follow the graph's edges.

A test trace or log trace that has been matched to scenarios produces a sequence of scenario "hops" — each hop crosses a state-graph edge. For each consecutive pair of scenarios:

• If the graph has an edge between their source nodes → the hop is supported
• If there's no edge → the hop is unsupported

Unsupported hops indicate either a behavior the spec doesn't capture, an imprecise scenario match, or a missing edge in the reachability analysis.

Trace reachability summary

Aggregated across all traces, the summary reports:

• Scenarios hit — which scenarios were exercised by at least one trace
• Scenarios unhit — which scenarios have no trace coverage
• Top unsupported edges — the most common hops that the reachability graph doesn't support
• Frontier trace endings — scenarios where traces end at a sink or frontier node

This connects the formal model to real-world behavior, surfacing discrepancies between what the spec says is possible and what actually happens.

Reachability in the diff

When scenarios change, the state graph is recomputed. The diff tracks:

• Nodes added/removed (observed regions and sinks)
• Edges added/removed (scenario edges)
• Changes to the reachable/unreachable sets
• New or resolved safety violations
• New or resolved liveness violations

A good change increases connectivity (more nodes reachable) and resolves violations. An unexpected disconnection — a previously reachable node becoming unreachable, or a new sink appearing — indicates the change may have broken or under-specified a transition path.