CLI guide

SpecLogician uses typed "change" commands:

  • speclogician ch ... applies a change and creates a new state instance
  • speclogician view ... inspects state components
  • speclogician find ... searches for components
  • speclogician reach ... analyzes scenario reachability
  • speclogician undo rolls back changes

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

Change commands

Base model

speclogician ch base-edit --src "type state = { x : int; frozen : bool }\ntype action = { amount : int }"
speclogician ch base-edit --file ./base.iml

Predicates

speclogician ch pred-add --pred-type state --pred-name balance_ok --pred-src "s.x > 0"
speclogician ch pred-add --pred-type action --pred-name small_order --pred-src "a.amount <= 10000"
speclogician ch pred-edit --pred-name balance_ok --pred-src "s.x >= 0"
speclogician ch pred-remove --pred-name balance_ok

Transitions

speclogician ch trans-add --trans-name on_order --trans-src "{ x = s.x + a.amount; frozen = s.frozen }"
speclogician ch trans-edit --trans-name on_order --trans-src "{ x = s.x + a.amount; frozen = false }"
speclogician ch trans-remove --trans-name on_order

Scenarios

speclogician ch scenario-add accept_order --given balance_ok --when small_order --then on_order --goal
speclogician ch scenario-add boot --then on_order --initial
speclogician ch scenario-add crash --given invalid_state --then fail --bad
speclogician ch scenario-edit accept_order --given "+new_pred,-balance_ok"
speclogician ch scenario-edit crash --no-bad    # remove the bad flag
speclogician ch scenario-remove accept_order

Scenario flags: --initial (reachability root), --goal (must be reachable), --bad (must NOT be reachable). Use --no-goal / --no-bad to clear.

Traces

# Test trace
speclogician ch trace test-add --art-id T1 --name "test positive order" \
  --given "{ x = 100; frozen = false }" \
  --when "{ amount = 50 }" \
  --then "{ x = 150; frozen = false }" \
  --filepath "tests/test_orders.py" --language python
 
# Log trace
speclogician ch trace log-add --art-id L1 --filename "prod.log" \
  --given "{ x = 0; frozen = false }" \
  --when "{ amount = 100 }" \
  --then "{ x = 100; frozen = false }" \
  --contents "OrderAccepted qty=100"

Data artifacts

# Documentation reference
speclogician ch data doc-add --art-id D1 --text "Orders must be rejected if qty > 10000" --meta "From requirements.md"
 
# Source code reference
speclogician ch data src-add --art-id S1 --src-code "def check(order): return order.qty <= MAX_QTY" \
  --language python --file-path "risk/checks.py"

Artifact linking

Link artifacts to the model components they support:

speclogician ch data link --art-id D1 --comp-name small_order
speclogician ch data unlink --art-id D1 --comp-name small_order

Batch operations

Apply multiple changes in one pass. Analysis runs once at the end instead of after each change.

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

Input is a JSON array of change objects:

[
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "x_pos",
    "pred_src": "s.x > 0"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "step",
    "trans_src": "{ x = s.x + a.amount; frozen = s.frozen }"
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "sc1",
    "when": { "add": ["small_order"] },
    "then": { "add": ["step"] },
    "is_goal": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "crash",
    "given": { "add": ["x_pos"] },
    "is_bad": { "set": true }
  }
]

Scenario flags in batch JSON use {"set": true} or {"set": false} for is_initial, is_goal, and is_bad. Omit to leave unchanged.

Dry run

Validate a batch without applying it:

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

Returns { "ok": true, "dry_run": true, "changes_parsed": 3 } on success, or a structured error with change_index on failure.

Undo

Roll back the last change (moves it to an internal stash):

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

Agent prompt

Generate the full agent instruction guide:

speclogician prompt                    # print to stdout
speclogician prompt --out ./prompt.md  # write to file
Previous← Guides
NextView commands →