Past exam of the computer science course of the University of Oxford / 2015 / Concurrency / 2 / b / Solution

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.