soma.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.

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.

Generated from soma describe on this file.

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

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ 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

Builtins used

get_status, transition, valid_transitions

Source file: /corpus/state_machines/support_ticket.cell · examples/corpus/state_machines/support_ticket.cell