
\section{Channel Multiplexer Example}

     This section describes an application of the results of section
\ref{trans}, up to an including the results in \ref{ETM}.
The application is to a system of communication channels.
Each channel alternates transmission of forward and backward messages;
it repeatedly accepts a forward message through an event label $p$, delivers
it through an event labelled $q$, accepts a backward message
through an event labelled $r$ and delivers it through an event labelled
$s$.  In CSP the individual channel process can be written as
\begin{displaymath}
\symbol{CHAN} = \mu X \truethat \Choice_x p.x \rightarrow q.x \rightarrow
				\Choice_y r.y \rightarrow s.y \rightarrow X
\end{displaymath}
Sometimes the return message may be simply an acknowledgement,
leading to an implementation of synchronous unidirectional
channels.  Often many logical channels have
to be multiplexed over a single bidirectional line.  We assume the
availability of a line in each direction, each with an associated output
queuing mechanism whose details are abstracted by regarding queue plus
communication line as a FIFO.  Messages accepted by the FIFO are labelled
with the associated channel and the direction of the
FIFO ($f$ or $b$ for forward and backward lines), superfixed with $O$ or
$I$ according to whether the event is an output {\em to} the FIFO
or and input {\em from} the FIFO.  
\begin{eqnarray*}
\function{FIFO} (C, f, q) & = & (\Choice_{c \in C} \Choice_x c.f^O.x \rightarrow
       \function{FIFO} (C, f, q \concat \langle c.f^I.x \rangle)) \choice \\ &&
       (\bif q \not= \langle \rangle \bthen
	    q_0 \rightarrow \function {FIFO} (C, f, q') \belse \proc{STOP})
\end{eqnarray*}
Here $C$ is the set of channels recognised and $q$ is the set of
messages currently in the fifo---represented here, for brevity, as
a sequence of pending input events
(recollect that $\proc{STOP}$ is the unit of $\choice$, so when $q$ is
empty, outputs remain possible).  For each channel we introduce
in output buffer and an input buffer
\begin{displaymath}
\symbol{OBUF} = \mu X \truethat \Choice_x p.x \rightarrow f^O.x \rightarrow
				\Choice_y b^I.y \rightarrow s.y \rightarrow X
\end{displaymath}
\begin{displaymath}
\symbol{IBUF} = \mu X \truethat \Choice_x f^I.x \rightarrow q.x \rightarrow
				\Choice_y r.y \rightarrow b^O.y \rightarrow X
\end{displaymath}
The aim is to show that the system of buffers and FIFOs implements the
set of channels:
\begin{displaymath}
\begin{array}{l}
\left(
\left( \begin{array}{c} \Parallel \\ c \in \symbol{Chans} \end{array} c:\symbol{OBUF} \right) \parallel
\function{FIFO} (\symbol{Chans}, f, \langle \rangle) \parallel
\right. \\ \left. \,\,\,\,
\left( \begin{array}{c} \Parallel \\ c \in \symbol{Chans} \end{array} c:\symbol{IBUF}  \right) \parallel
\function{FIFO} (\symbol{Chans}, b, \langle \rangle)
\right) \setminus H =
\begin{array}{c} \Parallel \\ c \in \symbol{Chans} \end{array} c:\symbol{CHAN}
\end{array}
\end{displaymath}
where $H$ is the set of internal events
$\{ \any.f^O.\any \next \any.f^I.\any \next
\any.b^O.\any \next \any.b^I.\any \}$.

\subsection{Transition systems for buffers and FIFOs}

     First we write down simple TMs for the (deterministic)
components of the system
\footnote{In principle one should prove that these systems model the
CSP processes introduced above.  This could be done by using CSP proof
rules to determine the trace sets, then defining a mapping from traces
to the state spaces, as explained in section \ref{TM}.  Such a degree
of formality, when the correspondence is obvious anyway, seems
inappropriate here.}.
The channel processes and the buffers can be modelled on
the same state space
\begin{displaymath}
S^B = \alpha_0 \suchthat \alpha_1 \bof \symbol{Values} \suchthat
      \alpha_2 \suchthat \alpha_3 \bof \symbol{Values}
\end{displaymath}
where $\symbol{Values}$ is the set of values that can be transmitted
on a channel.  The transition functions for output and input buffers
are
\begin{eqnarray*}
T^O_c (\alpha_0) & = & \{ (c.p.\setvar{x} \mapsto \alpha_1 (\setvar{x})) \} \\
T^O_c (\alpha_1 (x)) & = & \{ (c.f^O.x \mapsto \alpha_2 ) \} \\
T^O_c (\alpha_2) & = & \{ (c.b^I.\setvar{x} \mapsto \alpha_3 (\setvar{x})) \} \\
T^O_c (\alpha_3 (x)) & = & \{ (c.s.x \mapsto \alpha_0 ) \}
\end{eqnarray*}
\begin{eqnarray*}
T^I_c (\alpha_0) & = & \{ (c.f^I.\setvar{x} \mapsto \alpha_1 (\setvar{x})) \} \\
T^I_c (\alpha_1 (x)) & = & \{ (c.q.x \mapsto \alpha_2 ) \} \\
T^I_c (\alpha_2) & = & \{ (c.r.\setvar{x} \mapsto \alpha_3 (\setvar{x})) \} \\
T^I_c (\alpha_3 (x)) & = & \{ (c.b^O.x \mapsto \alpha_0 ) \}.
\end{eqnarray*}
A fifo has state space $S^F = \symbol{CV}^*$, where $\symbol{CV} =
\symbol{Chans} \times \symbol{Values}$, and transition function
\begin{eqnarray*}
T^F_f (m) & = & \{ (\setvar{c}.f^O.\setvar{x} \mapsto
		  m \concat \langle (\setvar{c}, \setvar{x}) \rangle), \\ &&
               (\setvar{c}.f^I.\setvar{x} \mapsto m' \suchthat
		  m \not= \langle \rangle \land m_0 =
		   (\setvar{c}, \setvar{x})) \}
\end{eqnarray*}
According to section \ref{compose}, the complete system can be
represented on a state space which is the product of all the
component state spaces.  Where several of the components are
closely related, and indexed by elements of some set such
as $\symbol{Chans}$, it is convenient to group the associated
factors together in a function on the index space.  So the
composite state space can be taken as
\begin{displaymath}
S^{\scriptsym{MUX}} = (\symbol{Chans} \rightarrow S^B) \times S^F \times
                 (\symbol{Chans} \rightarrow S^B) \times S^F
\end{displaymath}
where the four factors correspond to output buffers, forward fifo,
input buffers and backward fifo respectively.
According to the expression in \ref{compose}, the transition
function on this system is given by
\def\setc{\setvar{c}}
\def\setx{\setvar{x}}
\begin{eqnarray*}
\lefteqn{T^{\scriptsym{MUX}} (O, m, I, n) =} \\ &&
\{
\begin{array}[t]{ll}
(\setc.p.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_1 (\setx))\}, m, I, n))
& \suchthat O (\setc) = \alpha_0, \\
(\setc.f^O.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_2)\},
  m \concat \langle (\setc, \setx) \rangle, I, n))
& \suchthat O (\setc) = \alpha_1 (\setx), \\
(\setc.f^I.\setx \mapsto (O, m', I \oplus \{(\setc \mapsto \alpha_1 (\setx))\},
  n))
& \suchthat m \not= \langle \rangle \land m_0 = (\setc, \setx) \land
  I (\setc) = \alpha_0, \\
(\setc.q.\setx \mapsto (O, m, I \oplus \{(\setc \mapsto \alpha_2)\}, n))
& \suchthat I (\setc) = \alpha_1 (\setx), \\
(\setc.r.\setx \mapsto (O, m, (I \oplus \{(\setc \mapsto \alpha_3 (\setx))\}, n))
& \suchthat I (\setc) = \alpha_2, \\
(\setc.b^O.\setx \mapsto (O, m, I \oplus \{(\setc \mapsto \alpha_0)\},
  n \concat \langle (\setc, \setx) \rangle))
& \suchthat I (\setc) = \alpha_3 (\setx), \\
(\setc.b^I.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_3 (\setx))\},
  m, I, n'))
& \suchthat n \not= \langle \rangle \land n_0 = (\setc, \setx) \land
  O (\setc) = \alpha_2, \\
(\setc.s.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_0)\}, m, I, n))
& \suchthat O (\setc) = \alpha_3 (\setx) \, \, \}
\end{array}
\end{eqnarray*}
The initial state is $(\{(\any \mapsto \alpha_0)\} \next \langle \rangle \next
\{(\any \mapsto \alpha_0)\} \next \langle \rangle )$.
Concealing internal events gives
\begin{eqnarray*}
\lefteqn{T^{\scriptsym{MUX2}} (O, m, I, n) =} \\ &&
\{ \begin{array}[t]{ll}
(\setc.p.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_1 (\setx))\}, m, I, n))
& \suchthat O (\setc) = \alpha_0, \\
(\setc.q.\setx \mapsto (O, m, I \oplus \{(\setc \mapsto \alpha_2)\}, n))
& \suchthat I (\setc) = \alpha_1 (\setx), \\
(\setc.r.\setx \mapsto (O, m, (I \oplus \{(\setc \mapsto \alpha_3 (\setx))\}, n))
& \suchthat I (\setc) = \alpha_2, \\
(\setc.s.\setx \mapsto (O \oplus \{(\setc \mapsto \alpha_0)\}, m, I, n))
& \suchthat O (\setc) = \alpha_3 (\setx) \, \, \}
\end{array} \\
\lefteqn{U^{\scriptsym{MUX2}} (O, m, I, n) =} \\ &&
\{ \begin{array}[t]{ll}
(O \oplus \{(\setc \mapsto \alpha_2)\},
  m \concat \langle (\setc, \setx) \rangle, I, n)
& \suchthat O (\setc) = \alpha_1 (\setx), \\
(O, m', I \oplus \{(\setc \mapsto \alpha_1 (\setx))\},
  n)
& \suchthat m \not= \langle \rangle \land m_0 = (\setc, \setx) \land
  I (\setc) = \alpha_0, \\
(O, m, I \oplus \{(\setc \mapsto \alpha_0)\},
  n \concat \langle (\setc, \setx) \rangle)
& \suchthat I (\setc) = \alpha_3 (\setx), \\
(O \oplus \{(\setc \mapsto \alpha_3 (\setx))\}, m, I, n')
& \suchthat n \not= \langle \rangle \land n_0 = (\setc, \setx) \land
  O (\setc) = \alpha_2 \, \, \}
\end{array}
\end{eqnarray*}
Now introduce the model
\begin{eqnarray*}
\lefteqn{T^{\scriptsym{CHANS}} (C) =} \\ &&
\{ \begin{array}[t]{ll}
(\setc.p.\setx \mapsto C \oplus \{(\setc \mapsto \alpha_1 (\setx))\})
& \suchthat C (\setc) = \alpha_0, \\
(\setc.q.\setx \mapsto C \oplus \{(\setc \mapsto \alpha_2)\})
& \suchthat C (\setc) = \alpha_1 (\setx), \\
(\setc.r.\setx \mapsto C \oplus \{(\setc \mapsto \alpha_3 (\setx))\})
& \suchthat C (\setc) = \alpha_2, \\
(\setc.s.\setx \mapsto C \oplus \{(\setc \mapsto \alpha_0)\})
& \suchthat C (\setc) = \alpha_3 (\setx) \, \, \}
\end{array}
\end{eqnarray*}
\begin{definition}
\label{def:Gdef}
The relationship $(O, m, I, n) \infix G C$ holds iff
for any $c$ one of the following (mutually exclusive) clauses obtains
%\begin{eqnarray}
%&&
%C (c) = \alpha_0 \land
%O (c) = \alpha_0 \land m \rhd \{(c, \any)\} = \langle \rangle \land
%I (c) = \alpha_0 \land n \rhd \{(c, \any)\} = \langle \rangle, \\&&
%C (c) = \alpha_1 (x) \land
%O (c) = \alpha_1 (x) \land m \rhd \{(c, \any)\} = \langle \rangle \land
%I (c) = \alpha_0 \land n \rhd \{(c, \any)\} = \langle \rangle, \\&&
%C (c) = \alpha_1 (x) \land
%O (c) = \alpha_2 \land m \rhd \{(c, \any)\} = \langle (c, x) \rangle \land
%I (c) = \alpha_0 \land n \rhd \{(c, \any)\} = \langle \rangle, \\&&
%C (c) = \alpha_1 (x) \land
%O (c) = \alpha_2 \land m \rhd \{(c, \any)\} = \langle \rangle \land
%I (c) = \alpha_1 (x) \land n \rhd \{(c, \any)\} = \langle \rangle, \\&&
%C (c) = \alpha_2 \land
%O (c) = \alpha_2 \land m \rhd \{(c, \any)\} = \langle \rangle \land
%I (c) = \alpha_2 \land n \rhd \{(c, \any)\} = \langle \rangle, \\&&
%C (c) = \alpha_3 (x) \land
%O (c) = \alpha_2 \land m \rhd \{(c, \any)\} = \langle \rangle \land
%I (c) = \alpha_3 (x) \land n \rhd \{(c, \any)\} = \langle \rangle, \\&&
%C (c) = \alpha_3 (x) \land
%O (c) = \alpha_2 \land m \rhd \{(c, \any)\} = \langle \rangle \land
%I (c) = \alpha_0 \land n \rhd \{(c, \any)\} = \langle (c, x) \rangle, \\&&
%C (c) = \alpha_3 (x) \land
%O (c) = \alpha_3 (x) \land m \rhd \{(c, \any)\} = \langle \rangle \land
%I (c) = \alpha_0 \land n \rhd \{(c, \any)\} = \langle \rangle
%\end{eqnarray}
\begin{eqnarray}
\lefteqn{C (c) = \alpha_0 \land} \nonumber \\&&
O (c) = \alpha_0 \land m \rhd \{(c, \any)\} = \langle \rangle \land
I (c) = \alpha_0 \land n \rhd \{(c, \any)\} = \langle \rangle, \\
\lefteqn{C (c) = \alpha_1 (x) \land} \nonumber \\&&
O (c) = \alpha_1 (x) \land m \rhd \{(c, \any)\} = \langle \rangle \land
I (c) = \alpha_0 \land n \rhd \{(c, \any)\} = \langle \rangle, \\
\lefteqn{C (c) = \alpha_1 (x) \land} \nonumber \\&&
O (c) = \alpha_2 \land m \rhd \{(c, \any)\} = \langle (c, x) \rangle \land
I (c) = \alpha_0 \land n \rhd \{(c, \any)\} = \langle \rangle, \\
\lefteqn{C (c) = \alpha_1 (x) \land} \nonumber \\&&
O (c) = \alpha_2 \land m \rhd \{(c, \any)\} = \langle \rangle \land
I (c) = \alpha_1 (x) \land n \rhd \{(c, \any)\} = \langle \rangle, \\
\lefteqn{C (c) = \alpha_2 \land} \nonumber \\&&
O (c) = \alpha_2 \land m \rhd \{(c, \any)\} = \langle \rangle \land
I (c) = \alpha_2 \land n \rhd \{(c, \any)\} = \langle \rangle, \\
\lefteqn{C (c) = \alpha_3 (x) \land} \nonumber \\&&
O (c) = \alpha_2 \land m \rhd \{(c, \any)\} = \langle \rangle \land
I (c) = \alpha_3 (x) \land n \rhd \{(c, \any)\} = \langle \rangle, \\
\lefteqn{C (c) = \alpha_3 (x) \land} \nonumber \\&&
O (c) = \alpha_2 \land m \rhd \{(c, \any)\} = \langle \rangle \land
I (c) = \alpha_0 \land n \rhd \{(c, \any)\} = \langle (c, x) \rangle, \\
\lefteqn{C (c) = \alpha_3 (x) \land} \nonumber \\&&
O (c) = \alpha_3 (x) \land m \rhd \{(c, \any)\} = \langle \rangle \land
I (c) = \alpha_0 \land n \rhd \{(c, \any)\} = \langle \rangle
\end{eqnarray}
\end{definition}
Suppose $(O, m, I, n) \infix G C$, then the following lemmas hold
\begin{lemma}
\label{lem:DsubD}.
$\dom T^{\scriptsym{MUX2}} (O, m, I, n) \subset 
\dom T^{\scriptsym{CHANS}} (C)$.
\end{lemma}
\begin{proof}
From the definition $T^{\scriptsym{MUX2}}$
\begin{displaymath}
\dom T^{\scriptsym{MUX2}} (C) =
\{ \begin{array}[t]{l}
\setc.p.\any \suchthat O (\setc) = \alpha_0 , \\
\setc.q.\setx \suchthat I (\setc) = \alpha_1 (\setx) , \\
\setc.r.\any \suchthat I (\setc) = \alpha_2 , \\
\setc.s.\setx \suchthat O (\setc) = \alpha_3 (\setx) \,\, \}.
\end{array}
\end{displaymath}
From the definition of $G$,
\begin{eqnarray*}
O (\setc) = \alpha_0 & \Rightarrow & C (\setc) = \alpha_0 \\
I (\setc) = \alpha_1 (\setx) & \Rightarrow & C (\setc) = \alpha_1 (\setx) \\
I (\setc) = \alpha_2 & \Rightarrow & C (\setc) = \alpha_2 \\
O (\setc) = \alpha_3 (\setx) & \Rightarrow & C (\setc) = \alpha_3 (\setx)
\end{eqnarray*}
(each antecedent is only compatible with one of the eight clauses
in definition \ref{def:Gdef}---in order, clauses 1, 4, 5 and 8.
The consequents are part of the respective clauses).
From the definition $T^{\scriptsym{CHANS}}$
\begin{displaymath}
\dom T^{\scriptsym{CHANS}} (C) =
\{ \begin{array}[t]{l}
\setc.p.\any \suchthat C (\setc) = \alpha_0 , \\
\setc.q.\setx \suchthat C (\setc) = \alpha_1 (\setx) , \\
\setc.r.\any \suchthat C (\setc) = \alpha_2 , \\
\setc.s.\setx \suchthat C (\setc) = \alpha_3 (\setx) \,\, \}
\end{array}
\end{displaymath}
and the result follows.
\end{proof}
\begin{lemma}
$e \in \dom T^{\scriptsym{MUX2}} (O, m, I, n) \Rightarrow
T^{\scriptsym{MUX2}} (O, m, I, n) (e) \infix{G} 
T^{\scriptsym{CHANS}} (C) (e)$.
\end{lemma}
\begin{proof}
There are four possibilities:

Firstly, $e = c.p.x$ and $O (c) = \alpha_0$.  Clause 1
in definition \ref{def:Gdef} obtains so $m \rhd \{(c, \any)\} =
\langle \rangle $ and $I (c) = \alpha_0$ and
$n \rhd \{(c, \any)\} = \langle \rangle $.
The new state of the $\symbol{MUX2}$ system,
$(O \oplus \{(\setc \mapsto \alpha_1 (\setx))\}, m, I, n)$,
is therefore related to the new state of the $\symbol{CHANS}$
system,
$C \oplus \{(\setc \mapsto \alpha_1 (\setx))\}$, by clause 2.

Secondly, $e = c.q.x$ and $I (c) = \alpha_1 (x)$.
Clause 4 in definition \ref{def:Gdef} obtains so $O (c) = \alpha_2$,
$m \rhd \{(c, \any)\} = \langle \rangle$ and
$n \rhd \{(c, \any)\} = \langle \rangle$.
Hence the new state of the $\symbol{MUX2}$ system,
$(O, m, I \oplus \{(\setc \mapsto \alpha_2)\}, n)$,
is related to the new state,
$C \oplus \{(\setc \mapsto \alpha_2)\}$,
of the $\symbol{CHANS}$ system by clause 5.

     The third and fourth cases, $e = c.r.x$ and $e = c.s.x$ are handled
in the same way.
\end{proof}
\begin{lemma}
$(O^1, m^1, I^1, n^1) \in U^{\scriptsym{MUX2}} (O, m, I, n) \Rightarrow
(O^1, m^1, I^1, n^1) \infix{G} C$.
\end{lemma}
\begin{proof}
There are four ways for $(O^1, m^1, I^1, n^1) \in
U^{\scriptsym{MUX2}} (O, m, I, n)$ to be satisfied.

The first possibility is that for some $c$,
$O (c) = \alpha_1 (x)$.  This
is only possible if clause 2 in \ref{def:Gdef} holds.
Thus $C (c) = \alpha_1 (x)$,
$m \rhd \{(c, \any)\} = \langle \rangle$ and $I (c) = \alpha_0$
and $n \rhd \{(c, \any)\} = \langle \rangle$.
Consequently $(O^1, m^1, I^1, n^1) = (O \oplus \{(\setc \mapsto \alpha_2)\},
  m \concat \langle (\setc, \setx) \rangle, I, n)$.
is related to $C$ by clause 3 in definition \ref{def:Gdef}.

The second possibility is that $m \not= \langle \rangle \land m_0 = (c, x)
\land I (c) = \alpha_0$.  The only clause which allows $m \rhd \{(c, \any)\}
\not= \langle \rangle$ is clause 3.
So  $C (c) =
\alpha_1 (x)$, $O (c) = \alpha_2$ and $m \rhd \{(c, \any)\} =
\langle (c, x) \rangle$ (so $m' \rhd \{(c, \any)\} = \langle \rangle$,
since $m_0 = (c, x)$) and $n \rhd \{(c, \any)\} = \langle \rangle$.
Hence
$(O^1, m^1, I^1, n^1) = (O, m', I \oplus \{(\setc \mapsto \alpha_1 (x))\}, n)$
satisfies clause 4, and this state is indeed related to $C$.

The other two cases in the definition of $U^{\scriptsym{MUX2}}$ are
treated similarly.
\end{proof}
\begin{lemma}
$U^{\scriptsym{MUX2}} (O, m, I, n) = \emptyset \Rightarrow
\dom T^{\scriptsym{MUX2}} (O, m, I, n) =
\dom T^{\scriptsym{CHANS}} (C)$.
\end{lemma}
\begin{proof}
According to discussion in the proof of the previous lemma, we
can assume that for no $c$ do clauses 2, 3, 6 or 7 hold,
otherwise $U^{\scriptsym{MUX2}} (O, m, I, n)$ would not
be empty.  So for each $c$ one of clauses 1, 4, 5 or 8 obtains.
The result then follows from the discussion in the proof of
lemma \ref{lem:DsubD}.
\end{proof}

These lemmas establish that $G$ is a simulation.  Hence the
multiplexor system implements the channel system.

