Example: Shopping cart

This example models a shopping cart that supports adding items, applying discounts, checking out, and cancelling. It demonstrates variant types for cart status, multiple transitions, and scenarios that capture both happy and rejection paths.

The system

Items can be added to the cart (each with a quantity)
A percentage discount can be applied once
The cart can be checked out if the total is positive
The cart can be cancelled at any time before checkout
Once checked out or cancelled, no further modifications are allowed

Domain base

type cart_status = Open | CheckedOut | Cancelled
 
type op = AddItem | ApplyDiscount | Checkout | Cancel
 
type state = {
  total : int;
  item_count : int;
  discount_applied : int;
  status : cart_status
}
 
type action = {
  op : op;
  amount : int
}

Design notes:

cart_status is a variant — three distinct lifecycle states with no meaningless values.
discount_applied is an int used as a boolean flag (0 or 1). IML doesn't have a native boolean type, so this is the idiomatic pattern. Using an int here is appropriate because it tracks a count, not a category.
amount serves double duty: it's the item quantity for AddItem and the discount percentage for ApplyDiscount. For Checkout and Cancel, it's unused. This keeps the action type simple — in a larger model you might use nested variant payloads instead.

Predicates

State predicates

Name	IML body	Meaning
`is_open`	`s.status = Open`	Cart accepts modifications
`is_checked_out`	`s.status = CheckedOut`	Cart has been finalized
`is_cancelled`	`s.status = Cancelled`	Cart has been cancelled
`has_items`	`s.item_count > 0`	Cart is non-empty
`no_discount_yet`	`s.discount_applied = 0`	Discount hasn't been applied
`has_positive_total`	`s.total > 0`	Total is positive (can checkout)

Action predicates

Name	IML body	Meaning
`is_add_item`	`a.op = AddItem`	Adding an item
`is_apply_discount`	`a.op = ApplyDiscount`	Applying a discount
`is_checkout`	`a.op = Checkout`	Checking out
`is_cancel`	`a.op = Cancel`	Cancelling the cart

Transitions

Each transition returns a new state. Every field must be assigned.

`add_item`

{ total = s.total + a.amount;
  item_count = s.item_count + 1;
  discount_applied = s.discount_applied;
  status = s.status }

Adds the item's value to the total and increments the count. Everything else is unchanged.

`apply_discount`

{ total = s.total - (s.total * a.amount / 100);
  item_count = s.item_count;
  discount_applied = 1;
  status = s.status }

Reduces the total by the discount percentage. Marks the discount as applied.

`do_checkout`

{ total = s.total;
  item_count = s.item_count;
  discount_applied = s.discount_applied;
  status = CheckedOut }

Finalizes the cart. Only the status changes.

`do_cancel`

{ total = 0;
  item_count = 0;
  discount_applied = s.discount_applied;
  status = Cancelled }

Zeros out the cart and marks it cancelled.

`noop`

{ total = s.total;
  item_count = s.item_count;
  discount_applied = s.discount_applied;
  status = s.status }

Nothing changes — used for rejected operations.

Scenarios

Happy paths

Scenario	Given	When	Then	Flags
`add_first_item`	`is_open`	`is_add_item`	`add_item`	`initial`
`add_more_items`	`is_open`, `has_items`	`is_add_item`	`add_item`
`discount_on_cart`	`is_open`, `has_items`, `no_discount_yet`	`is_apply_discount`	`apply_discount`
`checkout_cart`	`is_open`, `has_items`, `has_positive_total`	`is_checkout`	`do_checkout`	`goal`
`cancel_cart`	`is_open`	`is_cancel`	`do_cancel`

Rejection paths

Scenario	Given	When	Then
`checkout_empty_cart`	`is_open`	`is_checkout`	`noop`
`double_discount`	`is_open`	`is_apply_discount`	`noop`
`modify_after_checkout`	`is_checked_out`	`is_add_item`	`noop`
`modify_after_cancel`	`is_cancelled`	`is_add_item`	`noop`

Notes on the scenarios:

add_first_item is marked initial — the system starts with an open, empty cart.
checkout_cart is marked goal — we want to verify that checkout is always reachable from the initial state.
checkout_empty_cart guards against checking out with no items. The given has is_open but not has_items, so it fires when the cart is open but empty.
double_discount fires when the no_discount_yet predicate is not in the given — meaning a discount was already applied. Note that this scenario's given only requires is_open, not no_discount_yet, so it covers the case where a discount was already applied.

Reachability

Starting from add_first_item:

[add_first_item] ──▶ [add_more_items] ──▶ [discount_on_cart]
       │                    │                      │
       │                    │                      │
       ▼                    ▼                      ▼
 [cancel_cart]       [checkout_cart]         [checkout_cart]
                          (goal)                 (goal)

All scenarios are reachable from the initial. The goal scenario checkout_cart is reachable via multiple paths — adding items then checking out, or adding items, applying a discount, then checking out.

The rejection scenarios are also reachable:

checkout_empty_cart — reachable at the initial state (open, empty cart)
double_discount — reachable after discount_on_cart fires
modify_after_checkout — reachable after checkout_cart
modify_after_cancel — reachable after cancel_cart

Complement analysis

Even with 9 scenarios, there are uncovered regions. For example:

Cancel after checkout — what happens if is_checked_out + is_cancel? Not modeled. You might add a noop scenario or decide that checkout is terminal.
Discount on empty cart — is_open + no_discount_yet + is_apply_discount without has_items. Should this be allowed? The model doesn't say.
Checkout after cancel — is_cancelled + is_checkout. Probably should be a noop.

The complement tells you exactly which combinations of predicates lack a matching scenario. This is how SpecLogician guides you toward completeness — not by demanding you model everything upfront, but by showing you what's missing after each iteration.

Key observations

Scenarios partition behavior. Each scenario covers one path. Together, they describe the system. The complement shows what's left.
Predicates are reusable. is_open appears in many scenarios. has_items appears in both happy and rejection paths. You define a predicate once and reference it everywhere.
Transitions are shared too. noop is used by all four rejection scenarios. add_item is used by both add_first_item and add_more_items.
The model is incremental. You don't need all 9 scenarios at once. Start with the happy path, check the complement, then add rejection scenarios to cover the gaps.

Building this model with the CLI

Define the model

# Domain base
speclogician ch base-edit --src "type cart_status = Open | CheckedOut | Cancelled
type op = AddItem | ApplyDiscount | Checkout | Cancel
type state = { total : int; item_count : int; discount_applied : int; status : cart_status }
type action = { op : op; amount : int }" --json
 
# State predicates
speclogician ch pred-add --pred-type state --pred-name is_open \
  --pred-src "s.status = Open" --json
speclogician ch pred-add --pred-type state --pred-name is_checked_out \
  --pred-src "s.status = CheckedOut" --json
speclogician ch pred-add --pred-type state --pred-name is_cancelled \
  --pred-src "s.status = Cancelled" --json
speclogician ch pred-add --pred-type state --pred-name has_items \
  --pred-src "s.item_count > 0" --json
speclogician ch pred-add --pred-type state --pred-name no_discount_yet \
  --pred-src "s.discount_applied = 0" --json
speclogician ch pred-add --pred-type state --pred-name has_positive_total \
  --pred-src "s.total > 0" --json
 
# Action predicates
speclogician ch pred-add --pred-type action --pred-name is_add_item \
  --pred-src "a.op = AddItem" --json
speclogician ch pred-add --pred-type action --pred-name is_apply_discount \
  --pred-src "a.op = ApplyDiscount" --json
speclogician ch pred-add --pred-type action --pred-name is_checkout \
  --pred-src "a.op = Checkout" --json
speclogician ch pred-add --pred-type action --pred-name is_cancel \
  --pred-src "a.op = Cancel" --json
 
# Transitions
speclogician ch trans-add --trans-name add_item \
  --trans-src "{ total = s.total + a.amount; item_count = s.item_count + 1; discount_applied = s.discount_applied; status = s.status }" --json
speclogician ch trans-add --trans-name apply_discount \
  --trans-src "{ total = s.total - (s.total * a.amount / 100); item_count = s.item_count; discount_applied = 1; status = s.status }" --json
speclogician ch trans-add --trans-name do_checkout \
  --trans-src "{ total = s.total; item_count = s.item_count; discount_applied = s.discount_applied; status = CheckedOut }" --json
speclogician ch trans-add --trans-name do_cancel \
  --trans-src "{ total = 0; item_count = 0; discount_applied = s.discount_applied; status = Cancelled }" --json
speclogician ch trans-add --trans-name noop \
  --trans-src "{ total = s.total; item_count = s.item_count; discount_applied = s.discount_applied; status = s.status }" --json
 
# Happy path scenarios
speclogician ch scenario-add add_first_item \
  --given is_open --when is_add_item --then add_item --initial --json
speclogician ch scenario-add add_more_items \
  --given is_open --given has_items --when is_add_item --then add_item --json
speclogician ch scenario-add discount_on_cart \
  --given is_open --given has_items --given no_discount_yet \
  --when is_apply_discount --then apply_discount --json
speclogician ch scenario-add checkout_cart \
  --given is_open --given has_items --given has_positive_total \
  --when is_checkout --then do_checkout --goal --json
speclogician ch scenario-add cancel_cart \
  --given is_open --when is_cancel --then do_cancel --json
 
# Rejection path scenarios
speclogician ch scenario-add checkout_empty_cart \
  --given is_open --when is_checkout --then noop --json
speclogician ch scenario-add double_discount \
  --given is_open --when is_apply_discount --then noop --json
speclogician ch scenario-add modify_after_checkout \
  --given is_checked_out --when is_add_item --then noop --json
speclogician ch scenario-add modify_after_cancel \
  --given is_cancelled --when is_add_item --then noop --json

Inspect and verify

speclogician view state --compact
speclogician reach summary --json

Using batch instead

[
  {
    "kind": "DomainModelBaseEdit",
    "new_base_src": "type cart_status = Open | CheckedOut | Cancelled\ntype op = AddItem | ApplyDiscount | Checkout | Cancel\ntype state = { total : int; item_count : int; discount_applied : int; status : cart_status }\ntype action = { op : op; amount : int }"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "is_open",
    "pred_src": "s.status = Open"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "is_checked_out",
    "pred_src": "s.status = CheckedOut"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "is_cancelled",
    "pred_src": "s.status = Cancelled"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "has_items",
    "pred_src": "s.item_count > 0"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "no_discount_yet",
    "pred_src": "s.discount_applied = 0"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "has_positive_total",
    "pred_src": "s.total > 0"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_add_item",
    "pred_src": "a.op = AddItem"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_apply_discount",
    "pred_src": "a.op = ApplyDiscount"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_checkout",
    "pred_src": "a.op = Checkout"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_cancel",
    "pred_src": "a.op = Cancel"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "add_item",
    "trans_src": "{ total = s.total + a.amount; item_count = s.item_count + 1; discount_applied = s.discount_applied; status = s.status }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "apply_discount",
    "trans_src": "{ total = s.total - (s.total * a.amount / 100); item_count = s.item_count; discount_applied = 1; status = s.status }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "do_checkout",
    "trans_src": "{ total = s.total; item_count = s.item_count; discount_applied = s.discount_applied; status = CheckedOut }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "do_cancel",
    "trans_src": "{ total = 0; item_count = 0; discount_applied = s.discount_applied; status = Cancelled }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "noop",
    "trans_src": "{ total = s.total; item_count = s.item_count; discount_applied = s.discount_applied; status = s.status }"
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "add_first_item",
    "given": { "add": ["is_open"] },
    "when": { "add": ["is_add_item"] },
    "then": { "add": ["add_item"] },
    "is_initial": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "add_more_items",
    "given": { "add": ["is_open", "has_items"] },
    "when": { "add": ["is_add_item"] },
    "then": { "add": ["add_item"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "discount_on_cart",
    "given": { "add": ["is_open", "has_items", "no_discount_yet"] },
    "when": { "add": ["is_apply_discount"] },
    "then": { "add": ["apply_discount"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "checkout_cart",
    "given": { "add": ["is_open", "has_items", "has_positive_total"] },
    "when": { "add": ["is_checkout"] },
    "then": { "add": ["do_checkout"] },
    "is_goal": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "cancel_cart",
    "given": { "add": ["is_open"] },
    "when": { "add": ["is_cancel"] },
    "then": { "add": ["do_cancel"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "checkout_empty_cart",
    "given": { "add": ["is_open"] },
    "when": { "add": ["is_checkout"] },
    "then": { "add": ["noop"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "double_discount",
    "given": { "add": ["is_open"] },
    "when": { "add": ["is_apply_discount"] },
    "then": { "add": ["noop"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "modify_after_checkout",
    "given": { "add": ["is_checked_out"] },
    "when": { "add": ["is_add_item"] },
    "then": { "add": ["noop"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "modify_after_cancel",
    "given": { "add": ["is_cancelled"] },
    "when": { "add": ["is_add_item"] },
    "then": { "add": ["noop"] }
  }
]

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