First commands

SpecLogician uses two main command groups:

speclogician ch ... — apply typed changes (creates a new state instance)
speclogician view ... — inspect the current state

All commands accept --json for machine-readable output.

Applying changes

# Edit the domain base types
speclogician ch base-edit --src "type state = { x : int }\ntype action = { y : int }"
 
# Add a predicate
speclogician ch pred-add --pred-type state --pred-name x_positive --pred-src "s.x > 0"
 
# Add a transition
speclogician ch trans-add --trans-name step --trans-src "{ x = s.x + a.y }"
 
# Add a scenario
speclogician ch scenario-add grow --given x_positive --then step --initial

Batch changes

For efficiency, apply multiple changes at once using a JSON file:

speclogician ch batch --file changes.json --json

Use --dry-run to validate without applying:

speclogician ch batch --dry-run --json --file changes.json

Inspecting state

speclogician view state --compact     # overview with stats
speclogician view diff                # what changed
speclogician view domain              # domain model only
speclogician view artifacts           # all artifacts

Reachability

speclogician reach summary            # node/edge counts, reachable sets
speclogician reach unreachable        # dead scenarios
speclogician reach frontier           # scenarios with no successors

Searching

speclogician find predicates "qty"    # search predicates
speclogician find transitions "order" # search transitions
speclogician find usages x_positive   # where a component is used

Undo

speclogician undo                     # revert last change
speclogician undo --steps 3           # revert last 3 changes

State file

By default, state is saved to sl_state.json in the current directory. Use --state-json to specify a custom path:

speclogician --state-json myspec.json ch batch --file changes.json --json