First 5 minutes

This walkthrough builds a formal model for a simple order validation rule: "orders must be rejected if quantity exceeds 10,000".

Designed for coding agents. Every SpecLogician CLI command is built to be issued by an LLM coding agent — typed flags, structured --json output, no interactive prompts. The walkthrough below is exactly what an agent would run; you can run it by hand to learn the surface.

Two commands worth knowing before you start:

speclogician --help                  # discover commands and flags
speclogician prompt --out agent.md   # generate the agent instruction guide

Hand agent.md to your coding agent before delegating modeling work — it's a self-contained guide to the modeling discipline and command surface.

1. Define the domain base

Start by defining what state and action look like:

speclogician ch base-edit --src "type state = { pos : int; rejected : int }
type action = { qty : int }"

2. Add predicates

Predicates classify state and actions. Create a complementary pair for the quantity boundary:

speclogician ch pred-add --pred-type action --pred-name qty_ok --pred-src "a.qty <= 10000"
speclogician ch pred-add --pred-type action --pred-name qty_too_big --pred-src "a.qty > 10000"

3. Add a transition

Transitions define how state evolves. This one handles both accept and reject:

speclogician ch trans-add --trans-name on_new_order --trans-src \
  "if a.qty > 10000 then { pos = s.pos; rejected = s.rejected + 1 }
   else { pos = s.pos + a.qty; rejected = s.rejected }"

4. Add scenarios

Each scenario captures one behavioral path:

speclogician ch scenario-add reject_large --when qty_too_big --then on_new_order --initial
speclogician ch scenario-add accept_small --when qty_ok --then on_new_order

5. Inspect the result

speclogician view state --compact     # summary of everything
speclogician view diff                # what changed since last state
speclogician reach summary            # reachability analysis

You now have a formal model with:

• 2 predicates (complementary pair)
• 1 transition (branching logic)
• 2 scenarios (one per behavioral path)
• Symbolic complement analysis showing uncovered regions
• Reachability graph connecting scenarios

Every piece is machine-checked by ImandraX.

Next: safety and liveness

Once your model grows, mark desired outcomes as --goal and failure modes as --bad, then use reach properties to verify:

speclogician ch scenario-edit accept_small --goal
speclogician reach properties    # SAFE? LIVE?

See Reachability commands for details.