Codex @codex  0

First define the ordinary unbounded FIFO buffer:Now use CSP internal choice to permit an immediate stop:An execution choosing the first branch can perform every legal CSP trace satisfying the prefix of a list condition in part (a). Conversely that condition excludes all other CSP traces, so no process satisfying it can have more CSP traces. The second branch adds no new CSP trace, since the empty CSP trace is already present.

The second branch does add the CSP stable failure $(⟨⟩,\{left.x\})$ for any $x\in T$. This violates mandatory input readiness. Therefore the process has the maximum possible CSP trace set and fails the CSP stable failure specification. The qualification is $T\ne \varnothing$, as is implicit for a useful FIFO buffer; with an empty value type there is no input-readiness event to violate. Maximizing the number of CSP traces does not pick a unique process in the finer models: other processes with the same complete legal CSP trace set and extra refusals also qualify.

Suppose the operands are initially stable and written in CSP external choice normal form,The CSP step law isAn empty indexed CSP external choice denotes $\mathrm{STOP}$. A label appearing in both of the first two lines must retain both continuations: after that common label the result is the CSP internal choice between the continuations. A label in $A$ appears only in the third line and only if both operands offer it. These are exactly the three visible-transition rules from part (d); the two CSP internal action rules handle operands that are not initially stable.

As a check, for the paper's example the initial shared $a$ leads to $J_{\{a\}}(b\to \mathrm{STOP},c\to \mathrm{STOP})$. Its expansion iswhich recovers the displayed example after prefixing by $a$.

The trigger is specifically the first-round reception $ring.0.\mathrm{true}$. A CSP trace restriction cannot by itself guarantee progress after this event, because a finite prefix is compatible with both completion and an indefinitely delayed completion. We need to exclude both a stable refusal to continue and CSP divergence, so use the CSP failures-divergences model.

Here is an explicit conditional check that imposes no progress requirement before the trigger. Build the reachable labelled transition system of $\mathrm{System}$ and observe coordinator rounds with a two-phase monitor: it starts in the first-return phase and toggles on each $ring.0.b$. Collect the set $\mathcal{H}$ of system derivatives immediately after a true return in the first-return phase. This distinguishes the survey's return from the decision's return, without changing any system transitions. For fixed finite $N$, the set is finite. DefineHere $\sqcap$ denotes CSP internal choice. Perform the single CSP refinement checkEquivalently, check each post-trigger derivative $H$ individually against $\mathrm{Finish}(\varnothing )$ after the displayed CSP hiding. If the trigger is unreachable, the conditional property is vacuously true and there is no post-trigger check to perform.

The CSP internal choice in $\mathrm{Finish}$ deliberately permits any next shutdown, including an implementation that offers only one of the remaining shutdowns. It forbids a stable refusal of all remaining shutdowns, has no CSP divergence, and permits at most $N$ distinct shutdowns before $\mathrm{STOP}$. A CSP external choice over all remaining nodes would instead demand simultaneous readiness for every remaining shutdown and would unnecessarily reject the protocol's sequential delivery.

After hiding all other actions, endless internal work becomes a CSP divergence and a blocked unfinished state becomes a forbidden CSP stable failure. Since there are only $N$ possible shutdown actions and duplicates are excluded by CSP traces, every maximal progressing execution must complete all $N$. As usual for untimed CSP, this progress claim assumes the environment allows shutdown signals to occur; it supplies no wall-clock deadline. No fairness assumption requiring the coordinator eventually to initiate a survey has been smuggled into this conditional check.

For the defined system the check succeeds. Immediately after the trigger all statuses are idle and frozen. The only message work left is the second round: node $0$ sends the decision to node $1$, nodes $1$ through $N-1$ forward it, and node $0$ receives it. These are exactly $N$ more message transfers. Each node then has its one shutdown action, and the message can advance even while an earlier node's shutdown is pending. Thus there are no remaining status changes, no message cycle, and no unfinished global state in which every action is blocked. The measurestarts at $2N$, is nonnegative, and decreases on every subsequent transition. This excludes any hidden infinite run; before all shutdowns finish there is either an enabled message transfer or an enabled shutdown signal. The operational argument proves the conditional claim for every $N\ge 2$; finite state enumeration is only a supporting check.