Reachability

Reachability analysis answers the question: can the system get from here to there? SpecLogician builds a directed graph of scenario-to-scenario transitions, 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 has scenarios as nodes and possible transitions as edges. An edge from scenario A to scenario B exists when:

Scenario A's transition produces a new state
That new state can satisfy scenario B's given predicates
There exists an action that satisfies scenario B's when predicates

In other words: after scenario A fires, is it possible for scenario B to fire next?

ImandraX checks this for every pair of scenarios (O(n²) checks). Each check is a formal satisfiability query — not a simulation or sampling. If ImandraX finds a satisfying assignment, the edge exists and the assignment is stored as a witness.

Example: Bank account

[deposit_when_active] ──▶ [withdraw_sufficient]
         │                        │
         │                        ▼
         ├──▶ [freeze_account] ──▶ [unfreeze_account]
         │         │                      │
         │         ▼                      │
         │   [blocked_when_frozen]        │
         │                                │
         ◀────────────────────────────────┘

After a deposit (active account), you can withdraw, freeze, or deposit again. After freezing, you can unfreeze or attempt a blocked operation. After unfreezing, you're back to active — deposits and withdrawals are possible again.

Initial scenarios

At least one scenario should be marked initial. Initial scenarios are the roots of the reachability analysis — the BFS starts from them.

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

From the initials, SpecLogician computes:

Reachable scenarios — all scenarios reachable via any path from an initial
Unreachable scenarios — scenarios with no path from any initial

An unreachable scenario might indicate:

A missing intermediate scenario (the graph has a gap)
A scenario that can only be reached from a state the system never enters
An error in the given predicates (too restrictive)

Safety properties

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

Is the bad scenario reachable from any initial scenario?

If not reachable → the property is SAFE. ImandraX has proved that no sequence of transitions from the initial state can reach the bad scenario.
If reachable → safety violation. SpecLogician reports the shortest path from an initial scenario to the bad scenario, showing the exact sequence of transitions.

Example

(* bad scenario: balance goes negative *)
negative_balance
  given: balance_negative    (* s.balance < 0 *)
  when:  is_withdrawal
  then:  do_withdraw
  flag:  bad

If the model correctly guards withdrawals with has_sufficient_funds, this scenario should be unreachable. If there's a path to it, the shortest path reveals exactly which sequence of scenarios bypasses the guard.

Liveness properties

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

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

If reachable → the property is LIVE. There exists a path from an initial state to the goal.
If not reachable → liveness violation. The goal is disconnected from the initial scenarios.

Example

(* goal scenario: successful checkout *)
checkout_cart
  given: is_open, has_items, has_positive_total
  when:  is_checkout
  then:  do_checkout
  flag:  goal

If checkout_cart is unreachable from add_first_item (the initial), something is wrong — maybe a missing intermediate scenario, or predicates that are too restrictive.

Frontier gaps

The frontier consists of reachable scenarios that have no outgoing edges to unreachable scenarios. Frontier gaps indicate places where the reachability graph "stops" — scenarios from which the model doesn't specify what happens next.

For example, if checkout_cart is reachable but has no successors, the model doesn't say what happens after checkout. This might be intentional (checkout is a terminal state) or might indicate missing post-checkout scenarios.

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 (via trace matching) produces a sequence of scenario "hops." For each consecutive pair of scenarios in the trace:

If the reachability graph has an edge between them → the hop is supported
If there's no edge → the hop is unsupported

Unsupported hops indicate either:

The trace exercises a behavior the formal model doesn't capture
The scenario matching is imprecise (the trace was matched to the wrong scenario)
The reachability analysis has a gap (a missing edge)

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 without a clear next step

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 reachability graph is recomputed. The diff tracks:

Nodes added/removed
Edges added/removed
Changes to the reachable/unreachable sets
New or resolved safety violations
New or resolved liveness violations

A good change increases connectivity (more scenarios reachable) and resolves violations. An unexpected disconnection — a previously reachable scenario becoming unreachable — indicates the change may have broken a transition path.