Reachability commands

SpecLogician computes a scenario reachability graph using ImandraX. Scenarios marked --initial are root nodes. The graph shows which scenarios can follow which, based on whether one scenario's transitions can produce a state satisfying another's predicates.

Beyond basic connectivity, SpecLogician checks safety (no bad scenario is reachable) and liveness (all goal scenarios are reachable) properties.

All commands accept --json.

Summary

Overview of the reachability graph:

speclogician reach summary --json

Reports node/edge counts, reachable/unreachable sets, initial scenarios, and safety/liveness status.

Safety

Check that no scenario marked --bad is reachable from any initial:

speclogician reach safety
speclogician reach safety --json

Reports SAFE (no bad scenario reachable) or UNSAFE with violation paths showing the shortest route from an initial to each reachable bad scenario.

{
  "safe": false,
  "bads_reachable": ["panicked"],
  "safety_violations": [
    { "bad": "panicked", "path": ["initial_state", "skip_guards", "panicked"] }
  ]
}

Liveness

Check that all scenarios marked --goal are reachable from initials:

speclogician reach liveness
speclogician reach liveness --json

Reports LIVE (all goals reachable) or NOT LIVE with unreachable goals listed.

{
  "live": false,
  "goals_unreachable": ["test_passes"],
  "liveness_violations": [{ "goal": "test_passes" }]
}

Properties (combined)

Run both safety and liveness checks in one command:

speclogician reach properties
speclogician reach properties --json

This is the recommended command for the refinement loop — it gives a single SAFE/LIVE verdict.

Unreachable scenarios

List scenarios that cannot be reached from any initial scenario:

speclogician reach unreachable

Unreachable scenarios indicate missing transitions or over-constrained predicates.

Successors and predecessors

Which scenarios can follow or precede a given scenario:

speclogician reach succ accept_order     # what can happen after accept_order?
speclogician reach pred reject_order     # what leads to reject_order?

Explain an edge

Why can (or can't) one scenario reach another:

speclogician reach explain-edge accept_order reject_order --json

Returns a reachability verdict and witness.

Shortest path

Find the shortest scenario path between two scenarios:

speclogician reach path boot reject_order

Frontier

Scenarios with no outgoing edges (potential modeling gaps):

speclogician reach frontier

These are "dead ends" in the specification — either the system truly terminates there, or you need to model more transitions.