= Solution
For a finite <CSP trace> $s$, let $L(s)$ be its sequence of values on $\mathit{left}$ and $O(s)$ its sequence of values on $\mathit{right}$, with channel names removed. Restrict the external alphabet to these two channels. The behavioural <CSP trace> specification for an unbounded <FIFO buffer> is
$$
\boxed{\forall s\in\operatorname{traces}(P):\quad O(s)\preceq L(s),}
$$
where $\preceq$ 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)\mathbin{\frown}q(s)$, so $q(s)$ is the pending <FIFO queue> content. Define the events that must remain available by
$$
E(q)=\{\mathit{left}.x:x\in T\}\cup\begin{cases}\varnothing,&q=\langle\rangle,\\\{\mathit{right}.\operatorname{head}(q)\},&q\ne\langle\rangle.\end{cases}
$$
In addition to the <CSP trace> condition, require the behavioural <CSP stable failure> condition
$$
\boxed{\forall(s,X)\in\operatorname{failures}(P):\quad X\cap E(q(s))=\varnothing.}
$$
Thus 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>.
Back to article page
