First 5 minutes

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

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.