Example: Bank account

This example formalizes a bank account with multiple operations: deposits, withdrawals, freeze, and unfreeze. It demonstrates algebraic data types, multi-operation modeling, and reachability analysis.

The system

Accounts support deposits and withdrawals
An account can be frozen, which blocks all transactions until unfrozen
Balance cannot go negative (withdrawals are rejected if insufficient funds)

Domain base

type account_status = Active | Frozen
 
type op_kind = Deposit | Withdraw | Freeze | Unfreeze
 
type state = { balance : int; status : account_status }
 
type action = { op : op_kind; amount : int }

Design notes:

account_status is a variant — two distinct lifecycle states with no meaningless values.
op_kind enumerates all four operations as a variant. With variants, the complement can only contain valid constructors — no meaningless values like op = 5.
amount serves as the transaction value for deposits and withdrawals. For freeze/unfreeze, it's unused.

Predicates

State predicates

Name	IML body	Meaning
`is_active`	`s.status = Active`	Account accepts transactions
`is_frozen`	`s.status = Frozen`	Account is frozen — transactions blocked

Action predicates

Name	IML body	Meaning
`is_deposit`	`a.op = Deposit`	Deposit operation
`is_withdrawal`	`a.op = Withdraw`	Withdrawal operation
`is_freeze`	`a.op = Freeze`	Freeze operation
`is_unfreeze`	`a.op = Unfreeze`	Unfreeze operation
`has_sufficient_funds`	`a.amount <= s.balance`	Withdrawal amount is within balance
`insufficient_funds`	`a.amount > s.balance`	Withdrawal amount exceeds balance

Transitions

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

`do_deposit`

{ balance = s.balance + a.amount; status = s.status }

Adds the deposit amount to the balance. Status unchanged.

`do_withdraw`

{ balance = s.balance - a.amount; status = s.status }

Subtracts the withdrawal amount from the balance. Status unchanged.

`do_freeze`

{ balance = s.balance; status = Frozen }

Freezes the account. Balance unchanged.

`do_unfreeze`

{ balance = s.balance; status = Active }

Unfreezes the account. Balance unchanged.

`noop`

{ balance = s.balance; status = s.status }

Nothing changes — used for rejected operations.

Scenarios

Happy paths

Scenario	Given	When	Then	Flags
`deposit_when_active`	`is_active`	`is_deposit`	`do_deposit`	`initial`
`withdraw_sufficient`	`is_active`	`is_withdrawal`, `has_sufficient_funds`	`do_withdraw`
`freeze_account`	`is_active`	`is_freeze`	`do_freeze`
`unfreeze_account`	`is_frozen`	`is_unfreeze`	`do_unfreeze`

Rejection paths

Scenario	Given	When	Then
`withdraw_insufficient`	`is_active`	`is_withdrawal`, `insufficient_funds`	`noop`
`blocked_when_frozen`	`is_frozen`	`is_deposit`	`noop`

Notes:

deposit_when_active is marked initial — the system starts with an active account.
withdraw_sufficient requires both is_withdrawal and has_sufficient_funds — both action predicates must hold.
blocked_when_frozen demonstrates that frozen accounts reject deposits. The complement will reveal other frozen+operation combinations that aren't modeled.

Reachability

Starting from deposit_when_active:

Active operations can lead to freeze → freeze leads to unfreeze → unfreeze returns to active operations
All 6 scenarios are reachable from the initial
The reachability graph shows a cycle between active and frozen states

Complement analysis

The complement reveals uncovered regions:

Frozen + withdrawal — what happens when a frozen account receives a withdrawal? (not just a deposit)
Frozen + freeze — what if a frozen account receives another freeze?
Active + unfreeze — what happens when an active account receives an unfreeze?

These gaps guide the next iteration: add more noop scenarios to explicitly model the rejected operations.

Building this model with the CLI

Collect evidence

speclogician ch data doc-add --art-id doc-001 \
  --text "Bank accounts support deposits and withdrawals. Account can be frozen, which blocks all transactions until unfrozen. Balance cannot go negative." \
  --meta "Core requirements" --json
 
speclogician ch data src-add --art-id src-001 \
  --src-code "class Account:
    def deposit(self, amount):
        if self.frozen: raise Frozen()
        self.balance += amount
    def withdraw(self, amount):
        if self.frozen: raise Frozen()
        if amount > self.balance: raise InsufficientFunds()
        self.balance -= amount" \
  --language python --file-path "account.py" --json

Define the model

# Domain base
speclogician ch base-edit --src "type account_status = Active | Frozen
type op_kind = Deposit | Withdraw | Freeze | Unfreeze
type state = { balance : int; status : account_status }
type action = { op : op_kind; amount : int }" --json
 
# State predicates
speclogician ch pred-add --pred-type state --pred-name is_active \
  --pred-src "s.status = Active" --json
speclogician ch pred-add --pred-type state --pred-name is_frozen \
  --pred-src "s.status = Frozen" --json
 
# Action predicates
speclogician ch pred-add --pred-type action --pred-name is_deposit \
  --pred-src "a.op = Deposit" --json
speclogician ch pred-add --pred-type action --pred-name is_withdrawal \
  --pred-src "a.op = Withdraw" --json
speclogician ch pred-add --pred-type action --pred-name is_freeze \
  --pred-src "a.op = Freeze" --json
speclogician ch pred-add --pred-type action --pred-name is_unfreeze \
  --pred-src "a.op = Unfreeze" --json
speclogician ch pred-add --pred-type action --pred-name has_sufficient_funds \
  --pred-src "a.amount <= s.balance" --json
speclogician ch pred-add --pred-type action --pred-name insufficient_funds \
  --pred-src "a.amount > s.balance" --json
 
# Transitions
speclogician ch trans-add --trans-name do_deposit \
  --trans-src "{ balance = s.balance + a.amount; status = s.status }" --json
speclogician ch trans-add --trans-name do_withdraw \
  --trans-src "{ balance = s.balance - a.amount; status = s.status }" --json
speclogician ch trans-add --trans-name do_freeze \
  --trans-src "{ balance = s.balance; status = Frozen }" --json
speclogician ch trans-add --trans-name do_unfreeze \
  --trans-src "{ balance = s.balance; status = Active }" --json
speclogician ch trans-add --trans-name noop \
  --trans-src "{ balance = s.balance; status = s.status }" --json
 
# Happy path scenarios
speclogician ch scenario-add deposit_when_active \
  --given is_active --when is_deposit --then do_deposit --initial --json
speclogician ch scenario-add withdraw_sufficient \
  --given is_active --when is_withdrawal --when has_sufficient_funds --then do_withdraw --json
speclogician ch scenario-add freeze_account \
  --given is_active --when is_freeze --then do_freeze --json
speclogician ch scenario-add unfreeze_account \
  --given is_frozen --when is_unfreeze --then do_unfreeze --json
 
# Rejection path scenarios
speclogician ch scenario-add withdraw_insufficient \
  --given is_active --when is_withdrawal --when insufficient_funds --then noop --json
speclogician ch scenario-add blocked_when_frozen \
  --given is_frozen --when is_deposit --then noop --json

Inspect and verify

speclogician view state --compact
speclogician reach summary --json
speclogician reach succ deposit_when_active --json    # what follows a deposit?
speclogician reach succ freeze_account --json          # what follows a freeze?

Expected:

6 scenarios, all reachable from deposit_when_active (the initial)
No unreachable scenarios
Active operations can lead to freeze, freeze leads to unfreeze, unfreeze returns to active operations

Using batch instead

[
  {
    "kind": "AddDocRef",
    "art_id": "doc-001",
    "text": "Bank accounts support deposits and withdrawals. Account can be frozen. Balance cannot go negative."
  },
  {
    "kind": "DomainModelBaseEdit",
    "new_base_src": "type account_status = Active | Frozen\ntype op_kind = Deposit | Withdraw | Freeze | Unfreeze\ntype state = { balance : int; status : account_status }\ntype action = { op : op_kind; amount : int }"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "is_active",
    "pred_src": "s.status = Active"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "is_frozen",
    "pred_src": "s.status = Frozen"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_deposit",
    "pred_src": "a.op = Deposit"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_withdrawal",
    "pred_src": "a.op = Withdraw"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_freeze",
    "pred_src": "a.op = Freeze"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_unfreeze",
    "pred_src": "a.op = Unfreeze"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "has_sufficient_funds",
    "pred_src": "a.amount <= s.balance"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "insufficient_funds",
    "pred_src": "a.amount > s.balance"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "do_deposit",
    "trans_src": "{ balance = s.balance + a.amount; status = s.status }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "do_withdraw",
    "trans_src": "{ balance = s.balance - a.amount; status = s.status }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "do_freeze",
    "trans_src": "{ balance = s.balance; status = Frozen }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "do_unfreeze",
    "trans_src": "{ balance = s.balance; status = Active }"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "noop",
    "trans_src": "{ balance = s.balance; status = s.status }"
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "deposit_when_active",
    "given": { "add": ["is_active"] },
    "when": { "add": ["is_deposit"] },
    "then": { "add": ["do_deposit"] },
    "is_initial": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "withdraw_sufficient",
    "given": { "add": ["is_active"] },
    "when": { "add": ["is_withdrawal", "has_sufficient_funds"] },
    "then": { "add": ["do_withdraw"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "withdraw_insufficient",
    "given": { "add": ["is_active"] },
    "when": { "add": ["is_withdrawal", "insufficient_funds"] },
    "then": { "add": ["noop"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "freeze_account",
    "given": { "add": ["is_active"] },
    "when": { "add": ["is_freeze"] },
    "then": { "add": ["do_freeze"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "unfreeze_account",
    "given": { "add": ["is_frozen"] },
    "when": { "add": ["is_unfreeze"] },
    "then": { "add": ["do_unfreeze"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "blocked_when_frozen",
    "given": { "add": ["is_frozen"] },
    "when": { "add": ["is_deposit"] },
    "then": { "add": ["noop"] }
  }
]

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