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" \
  --description "Account balance is non-negative."
speclogician ch pred-add --pred-type action --pred-name small_order --pred-src "a.amount <= 10000"
 
# Edit the source, the description, or both. On edit, --pred-src is optional —
# you can update prose without re-supplying the IML body. At least one of
# --pred-src or --description must be provided.
speclogician ch pred-edit --pred-name balance_ok --pred-src "s.x >= 0"
speclogician ch pred-edit --pred-name balance_ok --description "Updated prose only — no body change."
 
speclogician ch pred-remove --pred-name balance_ok

--description is optional, but recommended for predicates whose name and body don't already make the intent obvious (threshold/boundary predicates, anything tied to a magic constant). Skip it when the name is self-evident (is_logged_in).

Transitions

speclogician ch trans-add --trans-name on_order \
  --trans-src "{ x = s.x + a.amount; frozen = s.frozen }" \
  --description "Apply the order amount to the running position; freeze status unchanged."
 
# Same as predicates: --trans-src is optional on edit when --description is supplied.
speclogician ch trans-edit --trans-name on_order --trans-src "{ x = s.x + a.amount; frozen = false }"
speclogician ch trans-edit --trans-name on_order --description "Updated prose only."
 
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 \
  --description "Happy path — a within-limit order is accepted and the position grows."
speclogician ch scenario-add boot --then on_order --initial
speclogician ch scenario-add crash --given invalid_state --then fail --bad \
  --description "Safety invariant — the system must never reach this state."
 
speclogician ch scenario-edit accept_order --given "+new_pred,-balance_ok"
speclogician ch scenario-edit accept_order --description "Updated prose only."
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. --description is optional on both add and edit; description-only edits are allowed.

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",
    "description": "Position is strictly positive."
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "step",
    "trans_src": "{ x = s.x + a.amount; frozen = s.frozen }",
    "description": "Apply the action amount to the position."
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "sc1",
    "description": "Small-order happy path — the position grows by the amount.",
    "when": { "add": ["small_order"] },
    "then": { "add": ["step"] },
    "is_goal": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "crash",
    "description": "Safety claim — this state must never be reached.",
    "given": { "add": ["x_pos"] },
    "is_bad": { "set": true }
  },
  {
    "kind": "PredicateEdit",
    "pred_name": "x_pos",
    "description": "Description-only update — pred_src omitted."
  }
]

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

description is optional on every Add/Edit change. On PredicateEdit and TransitionEdit, both pred_src/trans_src and description are optional — supply at least one. This lets you batch-update prose without touching IML bodies.

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 →