
%\documentstyle[11pt,zed]{csart}
\documentstyle{csart}

\begin{document}

\sloppy

\def\dotdot{\mathinner{\ldotp\ldotp}}

\def\parallel{\mathinner{\,\|\,}}
\def\Parallel{\mathinner{\|}}

\def\cho#1#2#3{{\vcenter{\vbox{\hrule height.#3pt
		\hbox{\vrule width.#3pt height#2pt \kern#1pt
		\vrule width.#3pt}
		\hrule height.#3pt}}}}
\def\choi{\mathchoice\cho5{15}{48}\cho4{12}{45}\cho39{25}\cho26{21}}
\def\Choice{\mathop{\smash\choi\vphantom\sum}}

\def\choice{{\scriptstyle \Choice }}

\def\righti#1#2{{\mathclose>\llap{$#2\kern#1pt$}}}
\def\rightif{\mathchoice\righti{3}{\displaystyle|}\righti3{\textstyle|}\righti{2}{\scriptstyle|}\righti{2}{\scriptscriptstyle|}\,}
\def\lefti#1#2{{\mathopen<\llap{$#2\kern#1pt$}}}
\def\leftif{\,\mathchoice\lefti{2}{\displaystyle|}\lefti{2}{\textstyle|}\lefti{2}{\scriptstyle|}\lefti{1.5}{\scriptscriptstyle|}}

\newcommand{\proc}[1]{\mbox{\bf {#1}}}
\newcommand{\symbol}[1]{\mbox{\it {#1}}}
\newcommand{\function}[1]{\mbox{\it {#1}} \,}

\def\satisfies{\, \, \mbox {\bf sat}\, \,}

\def\lbag{[[}
\def\rbag{]]}

\def\ndchoice{\sqcap}
\def\suchthat{\, | \,}
\def\concat{\hat{\mbox{ }}}
\def\pling{\, ! \,}
\def\query{\, ? \,}
\def\seq{; \, \,}
\def\next{, \,}

\def\bif{\mbox{\bf if}\, \,}
\def\bthen{\, \, \mbox{\bf then}\, \,}
\def\belse{\, \, \mbox{\bf else}\, \,}

\def\bcase{\mbox{\bf case}\, \,}
\def\bof{\, \, \mbox{\bf of}\, \,}
\def\aof{\mbox{\bf of}}
\def\bwhere{\mbox{\bf where}\, \,}

\def\powset{\mbox{P}}

\def\tini{\function{ini}}
\def\tok{\symbol{ok}}
\def\tdat{\function{dat}}
\def\treq{\function{req}}
\def\tnew{\symbol{new}}
\def\tchg{\function{chg}}
\def\tacs{\function{acs}}
\def\tack{\symbol{ack}}
\def\tmov{\function{mov}}
\def\tin{\function{in}}
\def\tout{\function{out}}

\def\follow{\, \mbox{\^{ }} \,}
\def\flatten{\mbox{\^{ }}/ \,}

\section{The Port Process}

     The state of a port involves three variables
\begin{description}
\item{$E$:} name of C-channel end associated with this port.
\item{$Q$:} name of port currently attached to the {\em other} end of $E$.
\item{$s$:} state of port {\em vis a vis} communications in progess.
\end{description}
Additionally, $R$, $S$ and $T$ are local variables holding port names,
$F$ is a local variable holding a channel end name, and $e$ is a local
variable which holds a data value.
\begin{figure}
\begin{eqnarray*}
\proc{INIT} (Q, s) & = & \Choice_R P.R^I \query \tini (E, Q, s, n) \rightarrow
		  \proc {SKIP} \\ \\
\proc{SEND} & = & (P.E \query \tdat (e) \rightarrow
		   Q.P^O \pling \tdat (e) \rightarrow
		   s := \tdat (e) ) \quad \choice \\ &&
		  (P.E \query \treq \rightarrow
		   \Choice_R R.P \pling \tnew \rightarrow
		   Q.P^O \pling \treq (R) \rightarrow
		   s := \treq (R)) \\ \\
\proc{ACK} & = & 
     \begin{array}[t]{ccrcl}
	\bcase t & \aof & \tok      & \Rightarrow & 
			P.Q^I \query \tack \rightarrow t := \tack \\
	    & | & \tack & \Rightarrow & 
		E.P \pling \tack \rightarrow s, t := \tok, \tok
     \end{array} \\ \\
\proc{ACS} (R) & = & 
     \begin{array}[t]{ccrcl}
	\bcase t & \aof & \tok      & \Rightarrow & 
			P.R \query \tacs (F) \rightarrow t := \tacs (F) \\
	    & | & \tacs (F) & \Rightarrow & 
		E.P \pling \tacs (F) \rightarrow s, t := \tok, \tok
     \end{array} \\ \\
\proc{RECV} (Q) & = & (P.Q^I \query \tdat (e) \rightarrow
		       s := \tdat (e) ) \quad \choice \quad
		      (P.Q^I \query \treq (R) \rightarrow
		       s := \treq (R) ) \\ \\
\proc{DAT} (e) & = & 
     \begin{array}[t]{ccrcl}
	\bcase t & \aof & \tok      & \Rightarrow & 
			E.P \pling \tdat (e) \rightarrow t := \tdat \\
	    & | & \tdat & \Rightarrow & 
		P.E \query \tack \rightarrow
		Q.P^O \pling \tack \rightarrow s, t := \tok, \tok
     \end{array} \\ \\
\proc{REQ} (R) & = & 
     \begin{array}[t]{ccrcl}
	\bcase t & \aof & \tok      & \Rightarrow & 
			E.P \pling \treq     \rightarrow t := \treq \\
	    & | & \treq & \Rightarrow &
		P.E \query \tacs (F) \rightarrow t := \tacs (F) \\
	    & | & \tacs (F) & \Rightarrow &
		F.P \pling \tmov (R) \rightarrow s, t := \tok, \tok
     \end{array}
\end{eqnarray*}
\caption{\label{S} ``Subroutines'' of the port process.}
\end{figure}
\begin{figure}
\begin{eqnarray*}
\proc{SEED} (F) & = &
	     E, s, t, n := F, \tok, \tok, 0 \seq \\&&
	     Q :=
	      (\bcase F \bof
	      \tin (C) \Rightarrow \function{init} (\tout (C))
	      \suchthat \tout (C) \Rightarrow \function{init} (\tin (C))) \\ \\
\proc{NEW} & = & \Choice_R P.R \query \tnew \rightarrow 
		  \left( \proc{INIT} (Q, s) \quad \choice \quad
		  \vphantom{\Choice_S} \right. \\ &&
		  \Choice_S
		  (P.S^I \query \tchg (Q, n') \rightarrow
		  \proc{INIT} (Q', s) \seq P.S^O \pling \tchg (P, n) \rightarrow
		  \proc{SKIP}) \quad \choice
		  \\ &&
		  \Choice_S
		  (\left. \vphantom{\Choice_S}
		  \proc{RECV} (S) \rightarrow \proc{INIT} (Q, s') \seq
		  n := n + 1)
		  \right) \seq \\ &&
		  R.P \pling \tacs (E) \rightarrow t := \tok \\ \\
\proc{BEGIN} & = & \proc{SEED} (\symbol{init}^{-1} (P))
		   \leftif \symbol{init}^{-1} (P) \neq \symbol {null} \rightif
		   \proc{NEW} \\ \\
\proc{OUTPUT} & = & 
     \begin{array}[t]{ccrcl}
	\bcase s & \aof & \tok      & \Rightarrow & 
		      \proc{SEND} \seq n := n + 1 \\
	    & | & \tdat (e) & \Rightarrow & \proc{ACK} \\
	    & | & \treq (R) & \Rightarrow & \proc{ACS} (R)
     \end{array} \\ \\
\proc{INPUT} & = & 
     \begin{array}[t]{ccrcl}
       \bcase s & \aof & \tok      & \Rightarrow &
			      \proc{RECV} (Q) \seq n := n + 1 \\
	    & | & \tdat (e) & \Rightarrow & \proc{DAT} (e) \\
	    & | & \treq (T) & \Rightarrow & \proc{REQ} (R)
     \end{array} \\ \\
\proc{END} & = & P.E \query \tmov (S) \rightarrow
		  Q.P^O \pling \tchg (S, n) \rightarrow \\ &&
		  \Big( (\proc{RECV} (Q) \seq n := n + 1 \seq
		  P.Q^I \query \tchg (T, n') \rightarrow
		  Q := T) \quad \choice \\ &&
		  (P.Q^I \query \tchg (T, n') \rightarrow
		  ((\proc{RECV} (Q) \seq n := n + 1) \leftif n' \neq n \rightif
		  \proc{SKIP} ) \seq Q := T ) \Big) \seq \\ &&
		  S.P^O \pling \tini (E, Q, s, n) \rightarrow \\&&
		  (\bcase s, t \bof \treq (R), tacs (F) \Rightarrow
		      F.P \pling \tmov (R) \rightarrow \proc{STOP}
		     \suchthat \, \_ \, \Rightarrow \proc{STOP})
		  \\ \\
\proc{P} & = & \proc{BEGIN} \seq * (
	      \begin{array}[t]{l}
		(P.Q^I \query \tchg (R, n') \rightarrow
		 Q.P^O \pling \tchg (P, n) \rightarrow Q := R) \quad \choice \\
		(\bcase E \bof \tin (C) \Rightarrow \proc {INPUT}
		    \suchthat \tout (C) \Rightarrow \proc {OUTPUT})
		    \quad \choice \\
		 \proc{END} \, \, )
	      \end{array}
\end{eqnarray*}
\caption{\label{P} Implementation of an individual port.}
\end{figure}

% Add extra space after big \Choice operators.
% Raise little \choice operators slightly.

\section{The Channel End Processes}

     The state of a channel end involves a variable $P$---the
port the channel end is currently attached to.  If $E$ is the name
of the output end of a channel
\begin{eqnarray*}
\proc{MOVE} & = & \Choice_Q E.Q \query \tmov (R) \rightarrow
		  P.E \pling \tmov (R) \rightarrow P := R \seq \proc{E} \\ \\
\proc{E} & = &  
		\proc{MOVE} \quad \choice \\ &&
	       (E.U \query \tdat (e) \rightarrow
		P.E \pling \tdat (e) \rightarrow
		E.P \query \tack \rightarrow
		U.E \pling \tack \rightarrow \proc{E}) \quad \choice \\ &&
	       (E.U \query \treq \rightarrow
		P.E \pling \treq \rightarrow
		E.P \query \tacs (F) \rightarrow
		U.E \pling \tacs (F) \rightarrow \proc{E})
\end{eqnarray*}

     If $E$ is the name of the input end of a channel
\begin{eqnarray*}
\proc{E} & = & \proc{MOVE} \quad \choice \\ &&
	       (E.P \query \tdat (e) \rightarrow \\ &&
	       \quad (\proc{MOVE} \quad \choice \quad
		      U.E \pling \tdat (e) \rightarrow
		      E.U \query \tack \rightarrow
		      P.E \pling \tack \rightarrow
		      \proc{E})) \quad \choice \\ &&
	       (E.P \query \treq \rightarrow \\ &&
	       \quad (\proc{MOVE} \quad \choice \quad
		      U.E \pling \treq \rightarrow
		      E.U \query \tacs (F) \rightarrow
		      P.E \pling \tacs (F) \rightarrow
		      \proc{E}))
\end{eqnarray*}
with $\proc{MOVE}$ defined as above.

\section{External interface of the port system.}

     Some definitions:

     A useful function on event sequences (the content of the first
$\tmov$ message from $E$ appearing in $s$, or $\symbol{init}$ if
there is no such message):
\begin{eqnarray*}
\function{port} (E) (s) & = &
    (\bif r = \langle \rangle \bthen \function{init} (E) \belse
    (\bcase \function{message} (r_0) \bof \tmov (P) \Rightarrow P)) \\ &&
    \bwhere r = s \downarrow \function{Alph\_mov\_port} (E)
\end{eqnarray*}

     The specification that only one channel end owns a particular
port at any time:
\begin{eqnarray*}
\function{True} (P) (\symbol{tr}) & = &
  \forall E : \symbol{Ends} \cdot \forall F : \symbol{Ends} \cdot \\&&
  ( \function{port} (E) (\overline{\symbol {tr}}) = P \land
    \function{port} (F) (\overline{\symbol {tr}}) = P ) \Rightarrow
    E = F
\end{eqnarray*}

     The specification that a channel end always communicates with
``its own'' port:
\begin{eqnarray*}
\function{Faithful} (E) (\symbol{tr}) & = &
  (s = \langle \rangle \lor \\&&
  \function {channel} (s_0) =
  \function{port} (E) (s').E \lor
  \function {channel} (s_0) =
  E.\function{port} (E) (s') ) \\&&
  \bwhere
  s = \overline{\symbol{tr}} \downarrow \function{Alph\_end} (E)
\end{eqnarray*}

\begin{figure}
\begin{eqnarray*}
\function{Seq\_mov\_port} (E) & = &
  \{\langle P.E.\tmov (Q) \rangle \suchthat
    P \in \symbol{Ports} \land Q \in \symbol{Ports} \} \\
\function{Seq\_dat\_out} (E) & = &
  \{\langle P.E.\tdat (e) \next E.P.\tack \rangle \suchthat
    P \in \symbol{Ports} \land e \in \symbol{Values} \} \\
\function{Seq\_req\_out} (E) & = &
  \{\langle P.E.\treq \next E.P.\tacs (F) \rangle \suchthat
    P \in \symbol{Ports} \land F \in \symbol{Ends} \} \\
\function{Seq\_dat\_in} (E) & = &
  \{ \langle E.P.\tdat (e) \next P.E.mov (Q) \rangle \suchthat
     P \in \symbol{Ports} \land Q \in \symbol{Ports} \} \cup \\ &&
  \{ \langle E.P.\tdat (e) \next P.E.\tack \rangle \suchthat
    P \in \symbol{Ports} \land e \in \symbol{Values} \} \\
\function{Seq\_req\_in} (E) & = &
  \{ \langle E.P.\treq \next P.E.mov (Q) \rangle \suchthat
     P \in \symbol{Ports} \land Q \in \symbol{Ports} \} \\ &&
  \{ \langle E.P.\treq \next P.E.\tacs (F) \rangle \suchthat
     P \in \symbol{Ports} \land F \in \symbol{Ends} \} \\
\function{Seq\_end} (E) & = & \function{Seq\_mov\_port} (E) \cup \\&&
     \begin{array}[t]{ccrcl}
	\bcase E & \aof & \tout (C) & \Rightarrow &
	  (\function{Seq\_dat\_out} (E) \cup \function{Seq\_req\_out} (E)) \\
	    & \suchthat & \tin (C) & \Rightarrow &
	  (\function{Seq\_dat\_in} (E) \cup \function{Seq\_req\_in} (E))
     \end{array} \\\\
\function{Seq\_transf} (E) & = &
  \{ \langle P.\tin (C).\tacs (E) \next E.Q.\tmov (R) \next
	S.E.\tmov (R') \next \tout (C).T.\tacs (E) \rangle \suchthat \\&&
    \{ P, Q, R, R', S, T \} \subset \symbol{Ports} \land C \in \symbol{Channels} \} \\\\
\function{Seq\_dat\_com} (C) & = &
  \{\langle P.\tout (C).\tdat (e) \rangle \follow a \follow \\&&
       \langle \tin (C).Q.\tdat (e) \next
	    Q.\tin (C).\tack \next \tout (C).P.\tack \rangle \suchthat \\&&
    \{ P, Q \} \subset \symbol{Ports} \land e \in \symbol{Values}
     \land a \in A (e)^* \} \\&&
     \bwhere A (e) =
     \{ in(C).R.\tdat (e) \suchthat R \in \symbol {Ports} \} \\
\function{Seq\_req\_com} (C) & = &
  \{\langle P.\tout (C).\treq \rangle \follow a \follow \\&&
       \langle \tin (C).Q.\treq \next
    Q.\tin (C).\tacs (F) \next \tout (C).P.\tacs (F) \rangle \suchthat \\&&
    \{ P, Q \} \subset \symbol{Ports} \land F \in \symbol{Ends}
     \land a \in A^* \} \\&&
     \bwhere A =
     \{ in(C).R.\treq \suchthat R \in \symbol {Ports} \} \\
\function{Seq\_chan} (C) & = &
   \function{Seq\_dat\_com} (C) \cup \function{Seq\_req\_com} (C) \\\\
\function{Seq\_mov} (E) & = &
  \{ \langle E.Q.\tmov (R) \next P.E.\tmov (R) \rangle \suchthat
    \{ P, Q, R \} \subset \symbol{Ports} \} \\\\
\function{Seq\_excl} (E) & = & 
  \{ \langle P.\tin (C).\tacs (E) \next 
	\tout (C).Q.\tacs (E) \rangle \suchthat %\\&&
    \{ P, Q \} \subset \symbol{Ports} \land C \in \symbol{Channels} \} \cup \\&&
     \begin{array}[t]{ccrcl}
	\bcase E & \aof & \tout (C) & \Rightarrow &
	  (\function{Seq\_dat\_out} (E) \cup \function{Seq\_req\_out} (E)) \\
	    & \suchthat & \tin (C) & \Rightarrow & \emptyset
     \end{array}
\end{eqnarray*}
\caption{\label{Seq} Some sub-sequences of the port system traces.}
\end{figure}

\begin{figure}
\begin{eqnarray*}
\function{Alph\_mov\_end} (E) & = &
     \{ E.P.\tmov (Q) \suchthat
	P \in \symbol{Ports} \land Q \in \symbol{Ports} \} \\
\function{Alph\_mov\_port} (E) & = &
     \{ P.E.\tmov (Q) \suchthat
	P \in \symbol{Ports} \land Q \in \symbol{Ports} \} \\
\function{Alph\_dat\_out} (E) & = & 
     \{ P.E.\tdat (e) \suchthat
	P \in \symbol{Ports} \land e \in \symbol{Values} \} \cup %\\ &&
     \{ E.P.\tack \suchthat P \in \symbol{Ports} \} \\
\function{Alph\_req\_out} (E) & = & 
     \{ P.E.\treq \suchthat P \in \symbol{Ports} \} \cup %\\ &&
     \{ E.P.\tacs (F) \suchthat
       P \in \symbol{Ports} \land F \in \symbol{Ends} \} \\
\function{Alph\_dat\_in} (E) & = & 
     \{ E.P.\tdat (e) \suchthat
	P \in \symbol{Ports} \land e \in \symbol{Values} \} \cup %\\ &&
     \{ P.E.\tack \suchthat P \in \symbol{Ports} \} \\
\function{Alph\_req\_in} (E) & = & 
     \{ E.P.\treq \suchthat P \in \symbol{Ports} \} \cup %\\ &&
     \{ P.E.\tacs (F) \suchthat
       P \in \symbol{Ports} \land F \in \symbol{Ends} \} \\
\function{Alph\_out} (E) & = & 
	\function{Alph\_dat\_out} (E) \cup \function{Alph\_req\_out} (E) \\
\function{Alph\_in} (E) & = & 
	\function{Alph\_dat\_in} (E) \cup \function{Alph\_req\_in} (E) \\
\function{Alph\_end} (E) & = & \function{Alph\_mov\_port} (E) \cup \\ &&
      (\bcase E \bof \tout (C) \Rightarrow \function{Alph\_out} (E)
	  \suchthat \tin (C) \Rightarrow \function{Alph\_in} (E)) \\
\function{Alph\_mov} (E) & = &
      \function{Alph\_mov\_end} (E) \cup \function{Alph\_mov\_port} (E) \\
\function{Alph\_acs} (E) & = & 
     \{ P.\tin (C).\tacs (E) \suchthat
	P \in \symbol{Ports} \land C \in \symbol{Channels} \} \cup \\ &&
     \{ \tout (C).P.\tacs (E) \suchthat
	P \in \symbol{Ports} \land C \in \symbol{Channels} \} \\
\function{Alph\_transf} (E) & = & \function{Alph\_mov} (E) \cup 
      \function{Alph\_acs} (E) \\
\function{Alph\_excl} (E) & = & 
    \function{Alph\_acs} (E) \cup %\\&&
      (\bcase E \bof \tout (C) \Rightarrow \function{Alph\_out} (E)
	    \suchthat \tin (C) \Rightarrow \emptyset ) \\
\function{Alph\_chan} (C) & = &
    \function{Alph\_out} (\tout (C)) \cup
    \function{Alph\_in} (\tin (C))
\end{eqnarray*}
\caption{\label{Alph} Some sub-sets of the port system alphabet.}
\end{figure}

     Introduce
\begin{eqnarray*}
\symbol{Prefix}^* (T) (\symbol{tr}) & = & \exists s : T^* \cdot
	   \symbol{tr} < \flatten s
\end{eqnarray*}
where $T$ is a set of event sequences.  This asserts that $\symbol{tr}$
is a prefix of some concatenation of the sequences in $T$.
Now introduce the specifications
\begin{eqnarray*}
\function{Good\_end} (E) (\symbol{tr}) & = &
  \symbol{Prefix}^* (\function{Seq\_end} (E))
  (\symbol{tr} \downarrow \function{Alph\_end} (E)) \\
\function{Good\_chan} (C) (\symbol{tr}) & = &
  \symbol{Prefix}^* (\function{Seq\_chan} (C))
  (\symbol{tr} \downarrow \function{Alph\_chan} (C)) \\
\function{Good\_transf} (E) (\symbol{tr}) & = &
  \symbol{Prefix}^* (\function{Seq\_transf} (E))
  (\symbol{tr} \downarrow \function{Alph\_transf} (E)) \\
\function{Good\_mov} (E) (\symbol{tr}) & = &
  \symbol{Prefix}^* (\function{Seq\_mov} (E))
  (\symbol{tr} \downarrow \function{Alph\_mov} (E)) \\
\function{Good\_excl} (E) (\symbol{tr}) & = &
  \symbol{Prefix}^* (\function{Seq\_excl} (E))
  (\symbol{tr} \downarrow \function{Alph\_excl} (E))
\end{eqnarray*}
and
\begin{eqnarray*}
\function{Ante} (\symbol{tr}) & = &
  \forall E :\symbol{Ends} \cdot \function{Good\_mov} (E) (\symbol{tr}) \land
                  \function{Good\_excl} (E) (\symbol{tr}) \\
\function{Vtrace} (\symbol{tr}) & = & 
  \function{Ante} (\symbol{tr}) \land \\&&
  \left( \forall E:\symbol{Ends}  \cdot
		  \function{Good\_end} (E) (\symbol{tr}) \land
                  \function{Good\_transf} (E) (\symbol{tr}) \land
                  \function{Faithful} (E) (\symbol{tr}) \right) \land \\&&
  \left( \forall C : \symbol{Channels} \cdot
    \function{Good\_chan} (C) (\symbol{tr}) \right) \land
  \left( \forall P : \symbol{Ports} \cdot
    \function{True} (P) (\symbol{tr}) \right)
\end{eqnarray*}
Finally, an attempt at a specification of the external interface of
the port system:
\begin{eqnarray*}
\function{Ante} (\symbol{tr}) \Rightarrow
\left( \function{Vtrace} (\symbol{tr}) \land
\forall c \cdot \function{Vtrace} (\langle c \rangle \follow \symbol{tr})
  \Rightarrow c \not\in \symbol{ref} \right)
\end{eqnarray*}
\end{document}

