= Solution
First define the ordinary unbounded <FIFO buffer>:
$$
\begin{aligned}
\mathrm{BUF}(q)&=\bigl(\mathit{left}?x:T\to\mathrm{BUF}(q\mathbin{\frown}\langle x\rangle)\bigr)\\
&\quad\mathbin\square\begin{cases}\mathrm{STOP},&q=\langle\rangle,\\\mathit{right}.\operatorname{head}(q)\to\mathrm{BUF}(\operatorname{tail}(q)),&q\ne\langle\rangle.\end{cases}
\end{aligned}
$$
Now use <CSP internal choice> to permit an immediate stop:
$$
\boxed{P=\mathrm{BUF}(\langle\rangle)\sqcap\mathrm{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> $(\langle\rangle,\{\mathit{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.
Back to article page
