wehub-resource-sync
84 lines
3.2 KiB
Plaintext
84 lines
3.2 KiB
Plaintext
---
|
|
# Authoritative formal design for realtime machine M3: response coordination.
|
|
#
|
|
# Companion to:
|
|
# - docs/design/realtime-state-machines.md (the map + invariants)
|
|
# - core/http/endpoints/openai/respcoord (the Go implementation)
|
|
#
|
|
# The Go MBT adapter maps each action below onto respcoord.Coordinator.Apply
|
|
# and the StateGetter onto respcoord.Coordinator.State, so this spec is the
|
|
# source of truth the implementation is checked against.
|
|
#
|
|
# NOTE: FizzBee is pre-1.0. Validate the exact syntax/CLI against the version
|
|
# pinned in formal-verification/README.md before trusting the gate.
|
|
deadlock_detection: false
|
|
---
|
|
|
|
# Bound the number of responses so the state space is finite.
|
|
MAX_RESPONSES = 4
|
|
|
|
role Session:
|
|
action Init:
|
|
self.live = 0 # number of live responses -- MUST stay in {0,1}
|
|
self.registered = 0 # id of the active response (0 = none)
|
|
self.next_id = 0
|
|
self.torn = 0 # session torn down (Terminated) -- absorbing
|
|
|
|
# startResponse as ONE indivisible transition -- this is the single-writer
|
|
# actor guarantee. Superseding an active response emits its cancelled
|
|
# terminal (live -= 1) BEFORE spawning the replacement (live += 1), so the
|
|
# net live count never exceeds 1.
|
|
#
|
|
# To reproduce the LEGACY dual-writer race from Part 2 of the design doc,
|
|
# change `atomic func` to `serial func`: the checker then interleaves two
|
|
# callers between the cancel and the spawn and reports AtMostOneLive
|
|
# violated -- exactly the bug TestLegacyMechanismCanDoubleStart pins in Go.
|
|
atomic func start():
|
|
if self.registered != 0:
|
|
self.live -= 1 # cancel + cancelled-terminal for the old
|
|
self.registered = 0
|
|
self.next_id += 1
|
|
self.live += 1 # spawn + register the replacement
|
|
self.registered = self.next_id
|
|
|
|
# client read-loop path: response.create / manual input_audio_buffer.commit.
|
|
# Rejected once torn (no response starts after teardown).
|
|
atomic action StartFromClient:
|
|
require self.next_id < MAX_RESPONSES
|
|
require self.torn == 0
|
|
self.start()
|
|
|
|
# VAD goroutine path: end-of-speech commit / barge-in. Rejected once torn.
|
|
atomic action StartFromVad:
|
|
require self.next_id < MAX_RESPONSES
|
|
require self.torn == 0
|
|
self.start()
|
|
|
|
# a response reaches its own terminal (response.done completed)
|
|
atomic action FinishCurrent:
|
|
if self.registered != 0:
|
|
self.live -= 1
|
|
self.registered = 0
|
|
|
|
# explicit response.cancel with nothing newer queued
|
|
atomic action CancelReq:
|
|
if self.registered != 0:
|
|
self.live -= 1
|
|
self.registered = 0
|
|
|
|
# session teardown (M1 parent): cancel any in-flight response and go to the
|
|
# absorbing Terminated state, after which no response can start. This is what
|
|
# lets the connection's teardown guarantee no response outlives the session.
|
|
atomic action Shutdown:
|
|
if self.registered != 0:
|
|
self.live -= 1
|
|
self.registered = 0
|
|
self.torn = 1
|
|
|
|
action Init:
|
|
s = Session()
|
|
|
|
# SAFETY: at most one live response at any instant (Part 4, invariant #1).
|
|
always assertion AtMostOneLive:
|
|
return s.live >= 0 and s.live <= 1
|