A coin-operated turnstile — the textbook two-state machine, plus an out-of-service state reachable only via maintenance
Demonstrates a cyclic machine (locked <-> unlocked) with a generic transition handler so we can assert_fails on a jump that the machine forbids (you cannot go straight from locked to out_of_service without unlocking first). NOTE: every move needs a declared edge, including a move to the state the instance is already in (`locked -> locked` would have to be declared): a transition() with no edge raises invalid_transition.
A Soma program from the state_machines part of the verified corpus: 77 lines, cells Turnstile, TurnstileTests. It passes soma check with soma 3.2.4.
How it is built
The cell Turnstile declares 5 signals in its face: coin(id: String) -> String, walk_through(id: String) -> String, go(id: String, to: String) -> String, state_of(id: String) -> String and passes() -> Int; keeps 1 memory slot: stats (Map<String, Int>, persistent and consistent). Its state machine gate starts in locked and allows 4 transitions: locked -> unlocked, unlocked -> locked, unlocked -> out_of_service and out_of_service -> locked. Handlers: coin (line 32), walk_through (line 37), go (line 45), state_of (line 50) and passes (line 52).
The file also holds 1 test cell (TurnstileTests) with 8 assertions, run by soma test.
The source
turnstile.cell
// A coin-operated turnstile — the textbook two-state machine, plus an
// out-of-service state reachable only via maintenance. Demonstrates a
// cyclic machine (locked <-> unlocked) with a generic transition handler
// so we can assert_fails on a jump that the machine forbids (you cannot
// go straight from locked to out_of_service without unlocking first).
//
// NOTE: every move needs a declared edge, including a move to the state the
// instance is already in (`locked -> locked` would have to be declared): a
// transition() with no edge raises invalid_transition.
cell Turnstile {
face {
signal coin(id: String) -> String
signal walk_through(id: String) -> String
signal go(id: String, to: String) -> String
signal state_of(id: String) -> String
signal passes() -> Int
}
memory {
stats: Map<String, Int> [persistent, consistent]
}
state gate {
initial: locked
locked -> unlocked
unlocked -> locked
unlocked -> out_of_service
out_of_service -> locked
}
on coin(id: String) {
transition(id, "unlocked")
return get_status(id)
}
on walk_through(id: String) {
transition(id, "locked")
let n = stats.get("passes") ?? 0
stats.set("passes", n + 1)
return get_status(id)
}
// generic, machine-validated transition
on go(id: String, to: String) {
transition(id, to)
return get_status(id)
}
on state_of(id: String) { return get_status(id) }
on passes() { return stats.get("passes") ?? 0 }
}
cell test TurnstileTests {
rules {
// a fresh instance starts locked
assert state_of("t0") == "locked"
// coin unlocks, walking through re-locks and counts a pass
assert coin("t1") == "unlocked"
assert walk_through("t1") == "locked"
assert passes() == 1
// out_of_service can be entered from unlocked
assert go("t2", "unlocked") == "unlocked"
assert go("t2", "out_of_service") == "out_of_service"
// illegal: you cannot drop a locked turnstile straight to
// out_of_service — it must be unlocked first
assert_fails go("t3", "out_of_service")
// illegal: a state name that doesn't exist is rejected outright
assert_fails go("t4", "exploded")
}
}What the toolchain says
$ soma check turnstile.cell
✓ All checks passed.$ soma test turnstile.cell
test TurnstileTests ...
✓ assert state_of("t0") == "locked"
✓ assert coin("t1") == "unlocked"
✓ assert walk_through("t1") == "locked"
✓ assert passes() == 1
✓ assert go("t2", "unlocked") == "unlocked"
✓ assert go("t2", "out_of_service") == "out_of_service"
✓ assert_fails go("t3", "out_of_service") — raised invalid transition: locked → out_of_service. Current state: 'locked'. Valid targets: [unlocked]
✓ assert_fails go("t4", "exploded") — raised invalid transition: locked → exploded. Current state: 'locked'. Valid targets: [unlocked]
8 tests: 8 passed, 0 failed$ soma verify turnstile.cell
Verifying turnstile.cell...
State machine 'gate': 3 states, initial 'locked'
States: [locked, out_of_service, unlocked]
✓ 3 states, 4 transitions
✓ all states reachable from 'locked'
✓ reactive machine: no terminal state, and every reachable state can return to 'locked'
✓ no deadlocks
✓ liveness: every reachable state can return to 'locked' (reactive machine)
⚠ dynamic transition targets: handler `go` uses a dynamic (computed) transition target — the state these handlers move to is computed at run time (from input or an LLM answer), so the machine's safety is checked at run time for them, not proven
✓ termination: all 5 handlers structurally terminate
⚠ refinement (partial — dynamic targets fall back to runtime check): handler `go` calls transition() with a computed target — which edge it takes is checked at run time (invalid_transition), not proven; write the target as a literal state to have it verified
✓ refinement (partial — dynamic targets fall back to runtime check): handler `coin` ⟶ {unlocked}
✓ refinement (partial — dynamic targets fall back to runtime check): handler `walk_through` ⟶ {locked}
✓ refinement (partial — dynamic targets fall back to runtime check): handler `go` ⟶ <dynamic>
· transition sources: `coin`, `walk_through` call transition(id, target) without declaring the source — the runtime refuses a move the graph forbids, but the proof does not see where the handler starts; `transition(id, from, to)` names the edge (checked by `soma check`, refused at run time from any other state)
9 passed, 2 warnings, 0 failures
Temporal properties for 'gate':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK