Codex @codex  0

A process algebra in which components communicate through synchronized CSP events. Its operational description uses a labelled transition system; standard observations include CSP traces, CSP stable failures and CSP divergences.^[ref]

The alphabets assigned to participants determine their shared CSP events. An event in both assigned alphabets requires both participants; one assigned only to a single participant advances that participant. Replicated composition synchronizes all participants whose assigned alphabets contain the event.

Relabel visible CSP events according to a function or relation, preserving CSP internal actions. An injective relabelling preserves event identity; a non-injective one can merge distinct actions. In relational renaming, an original event with no image is disabled. Thus partial relational renaming can also restrict an interface.

Behave as $P$ until it performs a visible CSP event in $A$, then switch to $Q$. The triggering event is included in the visible CSP trace.

The first visible CSP event resolves the choice; the environment can select an event offered by only one branch. CSP internal actions can advance a branch without selecting it.

Turn CSP events in $A$ into CSP internal actions. Infinite hidden activity can create CSP divergence.

An unobservable transition that the environment cannot block. CSP hiding turns selected visible CSP events into CSP internal actions.

The process may internally choose either branch, independently of the environment's offered CSP events. Consequently it can have more CSP stable failures than the corresponding CSP external choice, despite having the same CSP traces.

Allow $P$ to proceed while $Q$ is ready to interrupt. The first visible CSP event of $Q$ discards $P$ and leaves the derivative of $Q$. A CSP internal action of $Q$ alone does not discard $P$.

Events in $A$ require both CSP processes; other visible CSP events advance one participant independently. CSP internal actions do not synchronize.

Perform CSP event $a$, then behave as CSP process $P$.

A component specified by possible CSP events and successor behaviours. $\mathrm{STOP}$ has no transitions. CSP prefixing, CSP choice and CSP parallel composition construct larger components.

An algebraic expansion listing the initially possible CSP events and their continuations. It translates operational transition cases into CSP external choice expressions.

A finite sequence of visible CSP events performed by a CSP process, omitting CSP internal actions.

§1.2, The CSP View of the World defines CSP events, CSP hiding, CSP refinement and the supported CSP semantic models. This source is cited for the meanings of the models, not for answers to the 2015 examination.

A transition system whose edges carry action labels. A CSP operational semantics uses visible CSP events and the internal label $\tau$.

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.

Take a fresh CSP event $h$ and defineThe apparent guard is removed by CSP hiding. Each unfolding can perform a CSP internal action and return to the same situation without any visible CSP event. Operationally this is an infinite internal loop, a CSP divergence, so the equation is not a guarded recursion. This is precisely why a syntactic test that counts every occurrence of $\to$ would be wrong.

Use a chain of identical storage cells, each retaining the first value it sees and passing later values to the next cell. On the return journey it passes the next cell's reversed output before emitting its own retained value. This turns the chain into a distributed LIFO stack.

Here is one cell template. Its ports $l,r$ carry incoming values towards the tail; $v,u$ carry returning values towards the front. Each port carries values in $T\cup \{end\}$, with the sentinel value outside $T$:An input such as $l?x:T$ abbreviates an indexed CSP external choice over the corresponding CSP events. An output $r!y$ is the CSP prefixing action $r.y$. There is no extra controller process.

For $n\ge 1$, take $n$ copies of this same template. Introduce channels $d_i,u_i$ for $0\le i\le n$ and apply port CSP event renaming to copy $i$, for $1\le i\le n$, as follows:At the front put $d_0=in$ and $u_0=out$. Adjacent cells synchronize on every shared $d_i$ or $u_i$ CSP event. The two tail channels $d_n,u_n$ are sentinel-only: $d_n.end$ and $u_n.end$ are local tail CSP events, with no other participant required. Disable all $d_n.x,u_n.x$ for $x\in T$. Formally, use a partial relational CSP event renaming for the last copy, omitting the pairs for its $r.x,v.x$ with $x\in T$; an unmapped transition is blocked. This explicitly prevents a fictitious tail from generating data.

Let $C_i$ be the resulting port-renamed cell and $A_i$ its visible alphabet. With $H$ consisting of the internal link CSP events, including the two tail CSP events, the answer isHere the indexed operator is CSP alphabetized parallel composition: each CSP event is synchronized by all cells whose alphabets contain it. There are exactly $n$ storage-cell processes; port wiring and the sentinel-only tail adapt their interfaces, without adding a helper process. The local tail CSP events are hidden, as are all inter-cell communications.

To see correctness, after inputs $x_1,\dots ,x_n$ have propagated, cell $i$ retains $x_i$. The input sentinel value propagates to the tail. The last cell performs its two local tail CSP events, then returns $x_n,end$. Inductively, if the suffix after cell $i$ returns $x_n,\dots ,x_{i+1},end$, cell $i$ relays those values, replaces the final sentinel value by $x_i,end$, and stops. Hence the external output isand starts only after $in.end$. Shared links provide synchronization rather than an assumption that all cells take steps simultaneously. For the degenerate known-empty input, no storage is needed: the interface is simply $in.end\to out.end\to \mathrm{STOP}$.

The obstruction is that the property is about where a transition originates, whereas the three standard CSP semantic models identify processes that can disagree about this fact. Take fresh $h\ne a$ and compareIn $G$, the only $a$ transition leaves a CSP stable state, so the property holds. Initially $B$ has both an $a$ transition to $\mathrm{STOP}$ and a CSP internal action to $a\to \mathrm{STOP}$. Its initial state is therefore not a CSP stable state, and its direct $a$ transition violates the property.

Nevertheless both have exactly the CSP traces $⟨⟩$ and $⟨a⟩$. Initially their possible stable observations offer exactly $a$, so their initial CSP stable failures are precisely $(⟨⟩,X)$ with $a\notin X$. After $a$, both can refuse every CSP event. Neither has a CSP divergence: the hidden $h$ can occur at most once. ThereforeNo CSP refinement test in one of these models can separate semantically equal operands. This also rules out placing the operand in a fixed context of ordinary CSP operators before the test, since those operators respect the model's equality. A model recording more about the interleaving of stability and acceptance, or an additional operator that explicitly observes stability, would be needed.