= Solution
This is a <safety property>: a bad shutdown or a later reactivation has a finite bad <CSP trace>. Use the <CSP traces model>. Let $V=\{0,\ldots,N-1\}$, let $A\subseteq V$ track active nodes, and let $D\subseteq V$ track nodes that have announced shutdown. Let $\mathrm{Ring}$ contain every message <CSP event>. Define the following specification over the status-signal alphabet:
$$
\begin{aligned}
\mathrm{Safe}(A,D)
&=\mathop{\square}_{n\in A\setminus D}\mathit{idle}.n\to\mathrm{Safe}(A\setminus\{n\},D)\\
&\quad\mathbin\square\mathop{\square}_{\substack{n\in V\setminus(A\cup D)\\D=\varnothing}}\mathit{active}.n\to\mathrm{Safe}(A\cup\{n\},D)\\
&\quad\mathbin\square\mathop{\square}_{\substack{n\in V\setminus D\\A=\varnothing}}\mathit{shutdown}.n\to\mathrm{Safe}(A,D\cup\{n\}).
\end{aligned}
$$
Use the <CSP refinement> check
$$
\boxed{\mathrm{Safe}(V,\varnothing)\sqsubseteq_T\mathrm{System}\setminus\mathrm{Ring}.}
$$
The specification offers a shutdown only if the active set is empty, and offers no activation once $D$ is nonempty. A trace violating either requirement is therefore absent from the specification. Recording $D$ also prevents duplicate shutdowns and any status change by an already shut-down node. <CSP hiding> removes message details irrelevant to this finite bad-prefix check; a <CSP traces model> check alone does not assert eventual progress.
The system satisfies the check. After the first message has passed nodes $1,\ldots,i$, its bit is the <Boolean conjunction> of their being idle when sampled. Every sampled node is then frozen until it forwards the second-round decision. A true bit returning to node $0$ therefore means that every non-coordinator is idle and still frozen; the coordinator has itself remained idle. A true decision consequently reaches only idle nodes, each of which proceeds to shutdown rather than returning to $\mathrm{Free}$. No node can subsequently become active. A false decision permits no shutdown at all.
Back to article page
