= Solution
Use the intended nontrivial <ring network>, with $N\geq2$, and let $n\oplus1=(n+1)\bmod N$. A <CSP event> $\mathit{ring}.n.b$ is one synchronized transfer from the predecessor to receiver $n$, rather than a separate enqueue and dequeue. Let $s$ be the <Boolean> saying whether node $n$ is active. For $1\leq n<N$, define
$$
\begin{aligned}
V(n,s)&=\begin{cases}\mathit{idle}.n\to\mathrm{Free}(n,\mathrm{false}),&s=\mathrm{true},\\\mathit{active}.n\to\mathrm{Free}(n,\mathrm{true}),&s=\mathrm{false},\end{cases}\\
\mathrm{Free}(n,s)&=V(n,s)\mathbin\square\bigl(\mathit{ring}.n?b:\mathrm{Bool}\to\mathit{ring}.(n\oplus1).(b\land\neg s)\to\mathrm{Second}(n,s)\bigr),\\
\mathrm{Second}(n,s)&=\mathit{ring}.n?b:\mathrm{Bool}\to\mathit{ring}.(n\oplus1).b\to\begin{cases}\mathit{shutdown}.n\to\mathrm{STOP},&b=\mathrm{true},\\\mathrm{Free}(n,s),&b=\mathrm{false}.
\end{cases}
\end{aligned}
$$
Initially the node is active:
$$
\boxed{\mathrm{Node}(n)=\mathrm{Free}(n,\mathrm{true}).}
$$
The <CSP external choice> in $\mathrm{Free}$ always offers both possible incoming message values as well as the permitted status change. Thus a decision to change status cannot internally withdraw readiness to receive a message. When the first message arrives, an active node forces its forwarded bit to false; an idle node preserves the bit. The status $s$ is retained until the second-round message has been forwarded. Neither the forwarding prefix nor $\mathrm{Second}$ offers status-change events, enforcing the protocol's freeze. On a false second-round message the node resumes its previous status; on a true one it forwards the bit before announcing shutdown.
Back to article page
