Support-ticket lifecycle with a reopen path
open -> in_progress -> resolved -> closed, with a resolved -> reopened loop that funnels back to in_progress. The * -> closed catch-all and the reopened -> in_progress arrow keep the machine live: every state can still reach the terminal `closed`. assert_fails guards illegal skips.
A Soma program from the state_machines part of the verified corpus: 60 lines, cells TicketDesk, TicketTests. It passes soma check with soma 3.2.4.
How it is built
The cell TicketDesk declares 7 signals in its face: file(id: String) -> String, assign(id: String) -> String, resolve(id: String) -> String, reopen(id: String) -> String, close(id: String) -> String, status(id: String) -> String and next(id: String) -> List<String>. Its state machine ticket starts in open and allows 6 transitions: open -> in_progress, in_progress -> resolved, resolved -> reopened, reopened -> in_progress, resolved -> closed and * -> closed. closed is terminal. Handlers: file (line 28), assign (line 29), resolve (line 30), reopen (line 31), close (line 32), status (line 33) and next (line 34).
The file also holds 1 test cell (TicketTests) with 11 assertions, run by soma test.
The source
support_ticket.cell
// Support-ticket lifecycle with a reopen path.
// open -> in_progress -> resolved -> closed, with a resolved -> reopened
// loop that funnels back to in_progress. The * -> closed catch-all and the
// reopened -> in_progress arrow keep the machine live: every state can
// still reach the terminal `closed`. assert_fails guards illegal skips.
cell TicketDesk {
face {
signal file(id: String) -> String
signal assign(id: String) -> String
signal resolve(id: String) -> String
signal reopen(id: String) -> String
signal close(id: String) -> String
signal status(id: String) -> String
signal next(id: String) -> List<String>
}
state ticket {
initial: open
open -> in_progress
in_progress -> resolved
resolved -> reopened
reopened -> in_progress
resolved -> closed
* -> closed
}
on file(id: String) { return get_status(id) }
on assign(id: String) { transition(id, "in_progress") return get_status(id) }
on resolve(id: String) { transition(id, "resolved") return get_status(id) }
on reopen(id: String) { transition(id, "reopened") return get_status(id) }
on close(id: String) { transition(id, "closed") return get_status(id) }
on status(id: String) { return get_status(id) }
on next(id: String) { return valid_transitions(id) }
}
cell test TicketTests {
rules {
// happy path
assert file("k1") == "open"
assert assign("k1") == "in_progress"
assert resolve("k1") == "resolved"
assert close("k1") == "closed"
// reopen loop: resolved -> reopened -> in_progress
assert assign("k2") == "in_progress"
assert resolve("k2") == "resolved"
assert reopen("k2") == "reopened"
assert assign("k2") == "in_progress"
// any ticket can be closed via the * catch-all (here from open)
assert close("k3") == "closed"
// illegal: cannot resolve a ticket nobody has picked up (open)
assert_fails resolve("k4")
// illegal: cannot reopen something that was never resolved
assert_fails reopen("k5")
}
}What the toolchain says
$ soma check support_ticket.cell
✓ All checks passed.$ soma test support_ticket.cell
test TicketTests ...
✓ assert file("k1") == "open"
✓ assert assign("k1") == "in_progress"
✓ assert resolve("k1") == "resolved"
✓ assert close("k1") == "closed"
✓ assert assign("k2") == "in_progress"
✓ assert resolve("k2") == "resolved"
✓ assert reopen("k2") == "reopened"
✓ assert assign("k2") == "in_progress"
✓ assert close("k3") == "closed"
✓ assert_fails resolve("k4") — raised invalid transition: open → resolved. Current state: 'open'. Valid targets: [in_progress, closed]
✓ assert_fails reopen("k5") — raised invalid transition: open → reopened. Current state: 'open'. Valid targets: [in_progress, closed]
11 tests: 11 passed, 0 failed$ soma verify support_ticket.cell
Verifying support_ticket.cell...
State machine 'ticket': 5 states, initial 'open'
States: [closed, in_progress, open, reopened, resolved]
✓ 5 states, 9 transitions
✓ all states reachable from 'open'
✓ terminal states: [closed]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ wildcard transitions: * -> [closed]
✓ think-isolated: CTL safety properties hold regardless of LLM output (4 handlers, 4 literal transitions, 0 dynamic)
✓ termination: all 7 handlers structurally terminate
✓ refinement: handler `assign` ⟶ {in_progress}
✓ refinement: handler `resolve` ⟶ {resolved}
✓ refinement: handler `reopen` ⟶ {reopened}
✓ refinement: handler `close` ⟶ {closed}
· transition sources: `assign`, `resolve`, `reopen`, `close` 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)
12 passed, 0 warnings, 0 failures
Temporal properties for 'ticket':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK