Example: Handshake protocol

This example models a simple authentication protocol where a client must authenticate before entering the READY state. It demonstrates reachability analysis — proving that certain states can only be reached through specific paths.

The rule

A client must AUTH before entering READY state
If the token is invalid, the client stays in INIT and the rejection counter increments
READY is only allowed after successful AUTH

Domain base

type state = { phase : int; rejected : int }
type action = { kind : int; token_ok : int }

Here phase uses integer encoding (0 = INIT, 1 = AUTHED, 2 = READY) and kind encodes the action type (1 = AUTH, 2 = READY). In a refined model you'd use variant types, but this demo shows what happens with integer encoding — including the messier complement regions.

Predicates

State predicates

Name	IML body	Meaning
`in_init`	`s.phase = 0`	Client is in INIT phase
`in_authed`	`s.phase = 1`	Client has authenticated
`in_ready`	`s.phase = 2`	Client is in READY state

Action predicates

Name	IML body	Meaning
`is_auth`	`a.kind = 1`	AUTH action
`is_ready`	`a.kind = 2`	READY action
`token_ok`	`a.token_ok = 1`	Token is valid
`token_bad`	`a.token_ok = 0`	Token is invalid

Transition

A single transition handles all protocol logic:

(* step *)
if a.kind = 1 then
  (if a.token_ok = 1 then { phase = 1; rejected = s.rejected }
   else { phase = 0; rejected = s.rejected + 1 })
else if a.kind = 2 then
  (if s.phase = 1 then { phase = 2; rejected = s.rejected }
   else { phase = s.phase; rejected = s.rejected + 1 })
else { phase = s.phase; rejected = s.rejected }

The branching logic:

AUTH with good token → move to AUTHED
AUTH with bad token → stay in INIT, increment rejected
READY when already AUTHED → move to READY
READY when not AUTHED → stay put, increment rejected

Scenarios

Scenario	Given	When	Then	Meaning
`auth_success`	`in_init`	`is_auth`, `token_ok`	`step`	Successful authentication
`auth_fail`	`in_init`	`is_auth`, `token_bad`	`step`	Failed authentication
`ready_after_auth`	`in_authed`	`is_ready`	`step`	Enter READY after AUTH

Reachability analysis

With auth_success as the initial scenario, reachability analysis shows:

auth_success → ready_after_auth is reachable: after successful auth, the client can enter READY
auth_fail is reachable from the initial state (INIT)
ready_after_auth is only reachable through auth_success — you must authenticate first

This formally proves the protocol requirement: READY requires prior AUTH.

Complement gaps

The complement reveals uncovered regions, including:

in_init + is_ready — what happens if a client tries READY without authenticating? The transition handles it (stays in INIT, increments rejected), but there's no scenario for it.
Integer-encoding artifacts — regions with phase = 3, kind = 5, etc. that don't correspond to real protocol states. This is where variant types would help.

Key takeaway

Reachability analysis provides a formal proof that the READY state is only reachable through AUTH. This isn't a test that checks a few examples — it's a mathematical guarantee over all possible protocol executions. The complement also reveals that the integer encoding creates spurious gap regions that variant types would eliminate.

Building this model with the CLI

Define the model

# Domain base
speclogician ch base-edit --src "type state = { phase : int; rejected : int }
type action = { kind : int; token_ok : int }" --json
 
# State predicates
speclogician ch pred-add --pred-type state --pred-name in_init \
  --pred-src "s.phase = 0" --json
speclogician ch pred-add --pred-type state --pred-name in_authed \
  --pred-src "s.phase = 1" --json
speclogician ch pred-add --pred-type state --pred-name in_ready \
  --pred-src "s.phase = 2" --json
 
# Action predicates
speclogician ch pred-add --pred-type action --pred-name is_auth \
  --pred-src "a.kind = 1" --json
speclogician ch pred-add --pred-type action --pred-name is_ready \
  --pred-src "a.kind = 2" --json
speclogician ch pred-add --pred-type action --pred-name token_ok \
  --pred-src "a.token_ok = 1" --json
speclogician ch pred-add --pred-type action --pred-name token_bad \
  --pred-src "a.token_ok = 0" --json
 
# Transition
speclogician ch trans-add --trans-name step --trans-src \
  "if a.kind = 1 then
    (if a.token_ok = 1 then { phase = 1; rejected = s.rejected }
     else { phase = 0; rejected = s.rejected + 1 })
   else if a.kind = 2 then
    (if s.phase = 1 then { phase = 2; rejected = s.rejected }
     else { phase = s.phase; rejected = s.rejected + 1 })
   else { phase = s.phase; rejected = s.rejected }" --json
 
# Scenarios
speclogician ch scenario-add auth_success \
  --given in_init --when is_auth --when token_ok --then step --initial --json
speclogician ch scenario-add auth_fail \
  --given in_init --when is_auth --when token_bad --then step --json
speclogician ch scenario-add ready_after_auth \
  --given in_authed --when is_ready --then step --json

Inspect and verify

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

Using batch instead

[
  {
    "kind": "DomainModelBaseEdit",
    "new_base_src": "type state = { phase : int; rejected : int }\ntype action = { kind : int; token_ok : int }"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "in_init",
    "pred_src": "s.phase = 0"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "in_authed",
    "pred_src": "s.phase = 1"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "state",
    "pred_name": "in_ready",
    "pred_src": "s.phase = 2"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_auth",
    "pred_src": "a.kind = 1"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "is_ready",
    "pred_src": "a.kind = 2"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "token_ok",
    "pred_src": "a.token_ok = 1"
  },
  {
    "kind": "PredicateAdd",
    "pred_type": "action",
    "pred_name": "token_bad",
    "pred_src": "a.token_ok = 0"
  },
  {
    "kind": "TransitionAdd",
    "trans_name": "step",
    "trans_src": "if a.kind = 1 then (if a.token_ok = 1 then { phase = 1; rejected = s.rejected } else { phase = 0; rejected = s.rejected + 1 }) else if a.kind = 2 then (if s.phase = 1 then { phase = 2; rejected = s.rejected } else { phase = s.phase; rejected = s.rejected + 1 }) else { phase = s.phase; rejected = s.rejected }"
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "auth_success",
    "given": { "add": ["in_init"] },
    "when": { "add": ["is_auth", "token_ok"] },
    "then": { "add": ["step"] },
    "is_initial": { "set": true }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "auth_fail",
    "given": { "add": ["in_init"] },
    "when": { "add": ["is_auth", "token_bad"] },
    "then": { "add": ["step"] }
  },
  {
    "kind": "ScenarioAdd",
    "scenario_name": "ready_after_auth",
    "given": { "add": ["in_authed"] },
    "when": { "add": ["is_ready"] },
    "then": { "add": ["step"] }
  }
]

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