Parcel shipment tracking with a delivery-exception loop
created -> picked_up -> in_transit -> out_for_delivery -> delivered. A failed delivery attempt bounces out_for_delivery back to in_transit; a parcel can be returned_to_sender from in_transit. Both delivered and returned_to_sender are terminal, and reachable from every state.
A Soma program from the state_machines part of the verified corpus: 67 lines, cells ShipmentTracker, ShipmentTests. It passes soma check with soma 3.2.4.
How it is built
The cell ShipmentTracker declares 8 signals in its face: label(id: String) -> String, pickup(id: String) -> String, depart(id: String) -> String, out(id: String) -> String, attempt_failed(id: String) -> String, deliver(id: String) -> String, return_parcel(id: String) -> String and track(id: String) -> String. Its state machine parcel starts in created and allows 6 transitions: created -> picked_up, picked_up -> in_transit, in_transit -> out_for_delivery, out_for_delivery -> delivered, out_for_delivery -> in_transit and in_transit -> returned_to_sender. delivered and returned_to_sender are terminal. Handlers: label (line 29), pickup (line 30), depart (line 31), out (line 32), attempt_failed (line 33), deliver (line 34), return_parcel (line 35) and track (line 36).
The file also holds 1 test cell (ShipmentTests) with 16 assertions, run by soma test.
The source
shipment_tracking.cell
// Parcel shipment tracking with a delivery-exception loop.
// created -> picked_up -> in_transit -> out_for_delivery -> delivered.
// A failed delivery attempt bounces out_for_delivery back to in_transit;
// a parcel can be returned_to_sender from in_transit. Both delivered and
// returned_to_sender are terminal, and reachable from every state.
cell ShipmentTracker {
face {
signal label(id: String) -> String
signal pickup(id: String) -> String
signal depart(id: String) -> String
signal out(id: String) -> String
signal attempt_failed(id: String) -> String
signal deliver(id: String) -> String
signal return_parcel(id: String) -> String
signal track(id: String) -> String
}
state parcel {
initial: created
created -> picked_up
picked_up -> in_transit
in_transit -> out_for_delivery
out_for_delivery -> delivered
out_for_delivery -> in_transit
in_transit -> returned_to_sender
}
on label(id: String) { return get_status(id) }
on pickup(id: String) { transition(id, "picked_up") return get_status(id) }
on depart(id: String) { transition(id, "in_transit") return get_status(id) }
on out(id: String) { transition(id, "out_for_delivery") return get_status(id) }
on attempt_failed(id: String) { transition(id, "in_transit") return get_status(id) }
on deliver(id: String) { transition(id, "delivered") return get_status(id) }
on return_parcel(id: String) { transition(id, "returned_to_sender") return get_status(id) }
on track(id: String) { return get_status(id) }
}
cell test ShipmentTests {
rules {
// straight-through delivery
assert label("p1") == "created"
assert pickup("p1") == "picked_up"
assert depart("p1") == "in_transit"
assert out("p1") == "out_for_delivery"
assert deliver("p1") == "delivered"
// failed attempt bounces back, then succeeds
assert pickup("p2") == "picked_up"
assert depart("p2") == "in_transit"
assert out("p2") == "out_for_delivery"
assert attempt_failed("p2") == "in_transit"
assert out("p2") == "out_for_delivery"
assert deliver("p2") == "delivered"
// return to sender from in_transit
assert pickup("p3") == "picked_up"
assert depart("p3") == "in_transit"
assert return_parcel("p3") == "returned_to_sender"
// illegal: cannot deliver something never picked up
assert_fails deliver("p4")
// illegal: cannot put a freshly created parcel out for delivery
assert_fails out("p5")
}
}What the toolchain says
$ soma check shipment_tracking.cell
✓ All checks passed.$ soma test shipment_tracking.cell
test ShipmentTests ...
✓ assert label("p1") == "created"
✓ assert pickup("p1") == "picked_up"
✓ assert depart("p1") == "in_transit"
✓ assert out("p1") == "out_for_delivery"
✓ assert deliver("p1") == "delivered"
✓ assert pickup("p2") == "picked_up"
✓ assert depart("p2") == "in_transit"
✓ assert out("p2") == "out_for_delivery"
✓ assert attempt_failed("p2") == "in_transit"
✓ assert out("p2") == "out_for_delivery"
✓ assert deliver("p2") == "delivered"
✓ assert pickup("p3") == "picked_up"
✓ assert depart("p3") == "in_transit"
✓ assert return_parcel("p3") == "returned_to_sender"
✓ assert_fails deliver("p4") — raised invalid transition: created → delivered. Current state: 'created'. Valid targets: [picked_up]
✓ assert_fails out("p5") — raised invalid transition: created → out_for_delivery. Current state: 'created'. Valid targets: [picked_up]
16 tests: 16 passed, 0 failed$ soma verify shipment_tracking.cell
Verifying shipment_tracking.cell...
State machine 'parcel': 6 states, initial 'created'
States: [created, delivered, in_transit, out_for_delivery, picked_up, returned_to_sender]
✓ 6 states, 6 transitions
✓ all states reachable from 'created'
✓ terminal states: [delivered, returned_to_sender]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (6 handlers, 6 literal transitions, 0 dynamic)
✓ termination: all 8 handlers structurally terminate
✓ refinement: handler `pickup` ⟶ {picked_up}
✓ refinement: handler `depart` ⟶ {in_transit}
✓ refinement: handler `out` ⟶ {out_for_delivery}
✓ refinement: handler `attempt_failed` ⟶ {in_transit}
✓ refinement: handler `deliver` ⟶ {delivered}
✓ refinement: handler `return_parcel` ⟶ {returned_to_sender}
· transition sources: `pickup`, `depart`, `out`, `attempt_failed`, `deliver`, `return_parcel` 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)
13 passed, 0 warnings, 0 failures
Temporal properties for 'parcel':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK