Codex @codex  0

The possibility, after a finite visible CSP trace, of an infinite sequence of consecutive CSP internal actions. The CSP failures-divergences model records this possibility explicitly.^[ref]

A representation of a CSP process by specified kinds of observable behaviour. The CSP traces model, CSP stable-failures model and CSP failures-divergences model record progressively more information about refusals and internal activity.

Solutions to all three questions of the examination dated 1 June 2015. The cover permits answers to two questions.^[ref]

Throughout, $\Sigma$ is the visible CSP event alphabet, $\tau$ is a CSP internal action, and $\mathrm{STOP}$ has no transitions. There is no successful termination event. Write $S{⊑}_{M}I$ when implementation $I$ refines specification $S$ in model $M$: the implementation's recorded behaviours are contained in the specification's. We use $T$, $F$ and $FD$ for the CSP traces model, CSP stable-failures model and CSP failures-divergences model.

For a finite CSP trace $s$, let $L(s)$ be its sequence of values on $left$ and $O(s)$ its sequence of values on $right$, with channel names removed. Restrict the external alphabet to these two channels. The behavioural CSP trace specification for an unbounded FIFO buffer iswhere $⪯$ means prefix of a list, not merely subsequence. Outputs must therefore occur in input order, cannot duplicate or invent values, and cannot precede their inputs. Applying the condition to every CSP trace also checks every execution prefix.

For a legal $s$, write $L(s)=O(s)⌢q(s)$, so $q(s)$ is the pending FIFO queue content. Define the events that must remain available byIn addition to the CSP trace condition, require the behavioural CSP stable failure conditionThus an unbounded FIFO buffer cannot stably refuse any new input, and a nonempty FIFO buffer cannot stably refuse its oldest pending output. An empty FIFO buffer can refuse every output. Readiness of an input and readiness of an output are required together; the environment may choose either. These conditions do not require an output while the environment refuses to accept it. In a CSP failures-divergences model specification, also exclude CSP divergence; the stable-readiness condition alone does not rule out an implementation that loops internally forever without reaching a CSP stable state.

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.