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

\begin{document}

\sloppy

\newenvironment{linear}{\\ \begin{minipage}[t]{\textwidth}}{\end{minipage}}
% Prevents body from being split between pages.  Can't be used at start
% of a paragraph.  Not within an indented environment.

\newenvironment{linpar}{\begin{minipage}[t]{\textwidth}}{\end{minipage}}
% Prevents body from being split between pages.  Used at start
% of a paragraph.  Not within an indented environment.

%\newenvironment{linpar1}{\newlength{\ltormar} \setlength{\textwidth} \addtolength{\textwidth}{-\leftmargin} \begin{minipage}[t]{\ltormar}}{\end{minipage}}
% As above, but 1 level of list indentation.  Doesn't work

\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{\bvector}[1]{\mbox{\boldmath $#1$}}
\newcommand{\mysymbol}[1]{\mbox{\it {#1}}}
\newcommand{\scriptsym}[1]{\mbox{\scriptsize \it {#1}}}
\newcommand{\function}[1]{\mbox{\it {#1}} \,}

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

\def\BigS{\mbox{\bf S}}
\def\BigA{\mbox{\bf A}}
\def\BigT{\mbox{\bf T}}


\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{\mysymbol{ok}}
\def\tmes{\function{mes}}
\def\tchg{\function{chg}}
\def\tquo{\function{quo}}
\def\tin{\function{in}}
\def\tout{\function{out}}

\def\interleaves{\, \, \function{interleaves}}

\def\any{\,\_\,}

\def\seqsize{\mbox{\#}}

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

\section{The Port-Handler Process}

     A port may be ``initialised'' or ``uninitialised''.
An initialised port is associated from the outset with some channel
end $\tout (C)$ or $\tin (C)$.  It has a partner initialised port,
associated with the opposite channel end.  An uninitialised port
is bound to a channel end when it receives an $\tini $ message.

     The alphabet of the port handling process associated with $P$ contains
main control thread events
\begin{displaymath}
   \{ (P, \any)^I.\tini \any \next (\any, P)^O.\tini \any \},
\end{displaymath}
repointing events
\begin{displaymath}
\{ (P, \any)^I.\tchg \any \next
   (\any, P)^O.\tquo \any \next
   (\any, P)^O.\tchg \any \next
   (P, \any)^I.\tquo \any \},
\end{displaymath}
and communication events
\begin{displaymath}
    \{ (\any, P)^O.\tmes \any \}.
\end{displaymath}
For the time being, $\tmes$ inputs are omitted from the alphabet
of the port handler.

  The traces of the process satisfy the following predicates:
\begin{enumerate}
\item{(Channel end association).}
Suppose we have a port handler associated with an initialised
port $P$ bound to channel end $E$.  The trace of this process
restricted to $\tini$ input events and $\tmes$, $\tchg$, $\tquo$ and
$\tini$ outputs,
is a prefix of a sequence consisting of an arbitrary
string of events from
$\{ (\any, P)^O.\tmes (E, \any) \next
(\any, P)^O.\tquo (E, \any) \}$ concatentated with a final sequence from
$\{ \langle (\any, P)^O.\tchg (E, \any, \any) \next
(\any, P)^O.\tini (E, \any, \any) \rangle \}$.

For an uninitialised
port, the similarly restricted trace is a prefix of a sequence consisting
of an initial event from
$\{ (P, \any)^I.\tini (E, \any, \any) \}$,
for some $E$, followed by a sequence from the set described in the previous
paragraph (with $E$ fixed through the subsequent life of the port).
\item{(Repointing thread).}
The trace of the port handler restricted to repointing events
and $\tini$ outputs is a prefix of
a sequence from built from an arbitrary concatenation of sequences
from
$\{ \langle
(P, {Q^-}')^I.\tchg \any \next ({Q^-}', P)^O.\tquo \any
\rangle \}$,
followed by {\em one} sequence from
\begin{eqnarray*}
& \{ \langle (\any, P)^O.\tchg (\any, {P^+}', \any) \next
    (P, \any)^I.\tquo \any \next
    ({P^+}', P)^O.\tini \any \rangle, & \\ &
  \,\,\, \langle (\any, P)^O.\tchg (\any, {P^+}', \any) \next
    (P, \any)^I.\tchg \any \next 
    ({P^+}', P)^O.\tini \any \rangle \}.
\end{eqnarray*}
\item{(Partner port association).}
In any event from
\begin{displaymath}
\{ (Q, P)^O.\tmes \any \next
(Q, P)^O.\tchg \any \next
(\any, P)^O.\tini (\any, Q, \any) \}
\end{displaymath}
appearing in a trace, the $Q$ field must have the same value as the
$Q$ field in the most recent preceding event of type
$(P, \any)^I.\tchg (\any, Q, \any)$.
If there is no preceding $\tchg $ input, the $Q$ field must match
either the initial value for the partner port (if $P$ is initialised),
or the value in the trace's compulsory
$(P, \any)^I.\tini (\any, Q, \any)$
event (if it is uninitialised).
\end{enumerate}

These three predicates are a complete specification of the traces of the
port process---the process can engage in any event sequence allowed by them.
Together with the requirement the process be deterministic, they
completely define the process
\footnote{The predicates have been expressed in English, with just a
few elementary ideas, like restriction, prefix and concatenation.
I'm not aware of a widely used formal notation that
would capture these specifications very concisely.
Rather than invent a new notation here, I'll stick with English for a
``declarative'' style of specification, and immediately introduce state
transition models for the three predicates, which can be referred to
if the English is too ambiguous.}.

\subsection{Transition model for predicate 1}

The state space of the model is
\begin{displaymath}
    \BigS^1 = \alpha_0 \suchthat
	      \alpha_1 \bof \mysymbol{Ends} \suchthat
	      \alpha_2 \bof \mysymbol{Ends} \suchthat
	      \alpha_3
\end{displaymath}
The alphabet of the model is
\begin{displaymath}
    \BigA^1_P =
   \{ (P, \any)^I.\tini \any \next \any.P^O.\tini \any \next
      (\any, P)^O.\tmes \any \next
      (\any, P)^O.\tquo \any \next
      (\any, P)^O.\tchg \any \}
\end{displaymath}
Its transition function is
\begin{eqnarray*}
\BigT^1_P (\alpha_0) & = & \{ ((P, \any)^I.\tini (E', \any, \any)
				 \mapsto \alpha_1 (E')) \} \\ 
\BigT^1_P (\alpha_1 (E)) & = & \{ ((\any, P)^O.\tquo (E, \any)
				 \mapsto \alpha_1 (E)), \\ && \, \, \,
                                 ((\any, P)^O.\tmes (E, \any)
				 \mapsto \alpha_1 (E)), \\ && \, \, \,
                                 ((\any, P)^O.\tchg (E, \any, \any)
				 \mapsto \alpha_2 (E)) \} \\
\BigT^1_P (\alpha_2 (E)) & = & \{ ((\any, P)^O.\tini (E, \any, \any)
				 \mapsto \alpha_3) \} \\
\BigT^1_P (\alpha_3) & = & \{ \}
\end{eqnarray*}
If $P$ is an initialised port bound to $E$, the initial state is
$\alpha_1 (E)$; if it's an uninitialised port the initial state
is $\alpha_0$.

\subsection{Transition model for predicate 2}

The state space of the model is
\begin{displaymath}
    \BigS^2 = \beta_0 \suchthat
	      \beta'_0 \bof \mysymbol{Ports} \suchthat
	      \beta_1 \bof \mysymbol{Ports} \suchthat
	      \beta_2 \bof \mysymbol{Ports} \suchthat
	      \beta_3
\end{displaymath}
The alphabet of the model is
\begin{displaymath}
    \BigA^2_P =
      \{ (P, \any)^I.\tchg \any \next
	 (\any, P)^O.\tquo \any \next
	 (\any, P)^O.\tchg \any \next
	 (P, \any)^I.\tquo \any \next
	 (\any, P)^O.\tini \any \}.
\end{displaymath}
Its transition function is
\begin{eqnarray*}
\BigT^2_P (\beta_0) & = &
	      \{ ((P, {Q^-}')^I.\tchg \any
		 \mapsto \beta_0' ({Q^-}')), \\ && \, \, \,
		 ((\any, P)^O.\tchg (\any, {P^+}', \any)
		 \mapsto \beta_1 ({P^+}')) \} \\
\BigT^2_P (\beta'_0 (Q^-)) & = &
	      \{ ((Q^-, P)^O.\tquo \any
		 \mapsto \beta_0) \} \\
\BigT^2_P (\beta_1 (P^+)) & = &
	      \{ ((P, \any)^I.\tquo \any
		 \mapsto \beta_2 (P^+)), \\ && \, \, \,
	         ((P, \any)^I.\tchg \any
		 \mapsto \beta_2 (P^+)) \} \\
\BigT^2_P (\beta_2 (P^+)) & = &
	      \{ ((P^+, P)^O.\tini \any
	         \mapsto \beta_3) \} \\
\BigT^2_P (\beta_3) & = & \{ \}
\end{eqnarray*}
The initial state is $\beta_0$.

\subsection{Transition model for predicate 3}

The state space of the model is
\begin{displaymath}
    \BigS^3 = \gamma_0 \suchthat
	      \gamma_1 \bof \mysymbol{Ports}
\end{displaymath}
The alphabet of the model is
\begin{displaymath}
    \BigA^3_P =
      \{ (\any, P)^I.\tini \any \next
	 (P, \any)^I.\tchg \any \next
	 (\any, P)^O.\tmes \any \next
	 (\any, P)^O.\tchg \any \next
	 (\any, P)^O.\tini \any \}.
\end{displaymath}
Its transition function is
\begin{eqnarray*}
\BigT^3_P (\gamma_0) & = &
	      \{ ((P, \any)^I.\tchg (\any, Q', \any)
		 \mapsto \gamma_1 (Q')), \\ && \, \, \,
		 ((P, \any)^I.\tini (\any, Q', \any)
		 \mapsto \gamma_1 (Q')) \} \\
\BigT^3_P (\gamma_1 (Q)) & = &
	      \{ ((P, \any)^I.\tchg (\any, Q', \any)
		 \mapsto \gamma_1 (Q')), \\ && \, \, \,
		 ((P, \any)^I.\tini \any
		 \mapsto \gamma_1 (Q)), \\ && \, \, \,
		 ((Q, P)^O.\tmes \any
		 \mapsto \gamma_1 (Q)), \\ && \, \, \,
		 ((Q, P)^O.\tchg \any
		 \mapsto \gamma_1 (Q)), \\ && \, \, \,
		 ((\any, P)^O.\tini (\any, Q, \any)
		 \mapsto \gamma_1 (Q)) \}
\end{eqnarray*}
If $P$ is an initialised port with original partner $Q$, the initial state is
$\gamma_1 (Q)$; if it's an uninitialised port the initial state
is $\gamma_0$.

The three transition functions are illustrated schematically in
figure \ref{Tpred}.

Inspection of these models (possibly by reference to the diagrams)
should persuade that they respectively
generate exactly the sets of traces specified by the original
three predicates.

\begin{figure}

\begin{center}

\begin{picture}(150, 50)(0, 0)

\put(  0,   0){$\alpha_0$}
\put( 50,   0){$\alpha_1$}
\put(100,   0){$\alpha_2$}
\put(150,   0){$\alpha_3$}

\multiput(13, 3)(50, 0){3}{\vector(1, 0){35}}

\put( 20, -10){$\query \tini$}
\put( 70, -10){$\pling \tchg$}
\put(120, -10){$\pling \tini$}

\put(47, 20){\oval(30, 30)[l]}
\put(47, 35){\vector(1, 0){10}}
\put(57, 35){\line(1, 0){6}}
\put(63, 20){\oval(30, 30)[r]}

\put( 40,52){$\pling \tmes$}
\put( 40,42){$\pling \tquo$}

\end{picture}

\end{center}

\begin{center}

\begin{picture}(150, 120)(0, -20)

\put(  0,   0){$\beta_0$}
\put(  0,  50){$\beta'_0$}
\put( 50,   0){$\beta_1$}
\put(100,   0){$\beta_2$}
\put(150,   0){$\beta_3$}

\put(13, 3){\vector(1, 0){35}}
\put( 20, -10){$\pling \tchg$}

\put(113, 3){\vector(1, 0){35}}
\put(120, -10){$\pling \tini$}

\put(-3, 20){\oval(30, 30)[bl]}
\put(-18, 20){\vector(0, 1){10}}
\put(-18, 29){\line(0, 1){6}}
\put(-3, 35){\oval(30, 30)[tl]}
\put(-45, 24){$\query \tchg$}

\put(13, 35){\oval(30, 30)[tr]}
\put(28, 35){\vector(0, -1){10}}
\put(28, 26){\line(0, -1){6}}
\put(13, 20){\oval(30, 30)[br]}
\put( 30, 24){$\pling \tquo$}

\put(71, 10){\oval(30, 30)[tl]}
\put(86, 10){\oval(30, 30)[tr]}
\put(71, 25){\vector(1, 0){10}}
\put(81, 25){\line(1, 0){5}}
\put( 65,32){$\query \tquo$}

\put(71, -5){\oval(30, 30)[bl]}
\put(86, -5){\oval(30, 30)[br]}
\put(71, -20){\vector(1, 0){10}}
\put(81, -20){\line(1, 0){5}}
\put( 65, -30){$\query \tchg$}

\end{picture}

\end{center}

\begin{center}

\begin{picture}(150,100)(-25, -25)

\put(  0,   0){$\gamma_0$}
\put( 50,   0){$\gamma_1$}

\put(21, 10){\oval(30, 30)[tl]}
\put(36, 10){\oval(30, 30)[tr]}
\put(21, 25){\vector(1, 0){10}}
\put(31, 25){\line(1, 0){5}}
\put( 15,32){$\query \tini$}

\put(21, -5){\oval(30, 30)[bl]}
\put(36, -5){\oval(30, 30)[br]}
\put(21, -20){\vector(1, 0){10}}
\put(31, -20){\line(1, 0){5}}
\put( 15, -30){$\query \tchg$}

\put(71, 10){\oval(30, 30)[t]}
\put(71, -5){\oval(30, 30)[b]}
\put(86, 10){\vector(0, -1){10}}
\put(86, 0){\line(0, -1){5}}
\put( 87, 20){$\query \tini$}
\put( 87, 10){$\query \tchg$}
\put( 87,  0){$\pling \tmes$}
\put( 87,-10){$\pling \tchg$}
\put( 87,-20){$\pling \tini$}

\end{picture}

\end{center}

\caption{\label{Tpred}``Predicate'' state transition diagrams (schematic)}

\end{figure}

\subsection{The $\mysymbol{Pstat}$ transition model}

   The port-handling process is described by the conjunction of the
three predicates.  Consequently it can be modelled by the composition
of the three state transition models just introduced.  It's
convenient to introduce an equivalent model based on the state space
\begin{displaymath}
    \mysymbol{Pstat} = \begin{array}[t]{l}
		     \pi_0 \suchthat \\
		     \pi'_0 \bof \mysymbol{Ports} \times
			   \mysymbol{Ports} \suchthat \\
		     \pi_1 \bof \mysymbol{Ends} \times \mysymbol{Ports} \suchthat \\
		     \pi'_1 \bof \mysymbol{Ends} \times
			   \mysymbol{Ports} \times \mysymbol{Ports} \suchthat \\
		     \pi_2 \bof \mysymbol{Ends} \times
			   \mysymbol{Ports} \times \mysymbol{Ports} \suchthat \\
		     \pi_3 \bof \mysymbol{Ends} \times
			   \mysymbol{Ports} \times \mysymbol{Ports} \suchthat \\
		     \pi_4
		     \end{array}
\end{displaymath}
The alphabet of the model $\BigA^{\scriptsym{Pstat}}_P$ is the
full alphabet of the port process, which has been defined earlier.
Its transition function is
\begin{eqnarray*}
\BigT^{\scriptsym{Pstat}}_P (\pi_0) & = &
  \{ ((P, {Q^-}')^I.\tchg (\any, Q', \any)
		       \mapsto \pi'_0 (Q', {Q^-}')), \\ && \,\,\,
    ((P, \any)^I.\tini (E', Q', \any)
		       \mapsto \pi_1 (E', Q')) \} \\
\BigT^{\scriptsym{Pstat}}_P (\pi'_0 (Q, Q^-)) & = &
  \{ ((P, \any)^I.\tini (E', Q', \any)
		       \mapsto (\pi'_1 (E', Q, Q^-)) \} \\
\BigT^{\scriptsym{Pstat}}_P (\pi_1 (E, Q)) & = &
  \{ ((Q, P)^O.\tmes (E, \any)
		       \mapsto \pi_1 (E, Q)), \\ && \,\,\,
     ((P, {Q^-}')^I.\tchg (\any, Q', \any)
		       \mapsto \pi'_1 (E, Q', {Q^-}')), \\ && \,\,\,
     ((Q, P)^O.\tchg (E, {P^+}', \any)
		       \mapsto \pi_2 (E, Q, {P^+}')) \} \\
\BigT^{\scriptsym{Pstat}}_P (\pi'_1 (E, Q, Q^-)) & = &
  \{ ((Q, P)^O.\tmes (E, \any)
		       \mapsto \pi'_1 (E, Q, Q^-)), \\ && \,\,\,
     ((Q^-, P)^O.\tquo (E, \any)
		       \mapsto \pi_1 (E, Q)) \} \\
\BigT^{\scriptsym{Pstat}}_P (\pi_2 (E, Q, P^+)) & = &
  \{ ((P, \any)^I.\tquo \any
		       \mapsto \pi_3 (E, Q, P^+)), \\ && \,\,\,
     ((P, \any)^I.\tchg (\any, Q', \any)
		       \mapsto \pi_3 (E, Q', P^+)) \} \\
\BigT^{\scriptsym{Pstat}}_P (\pi_3 (E, Q, P^+)) & = &
  \{ ((P^+, P)^O.\tini (E, Q, \any)
		       \mapsto \pi_4) \} \\
\BigT^{\scriptsym{Pstat}}_P (\pi_4) & = & \{ \}
\end{eqnarray*}
If $P$ is an initialised port bound to $E$, the initial state is
$\pi_1 (E, Q)$; if it's an uninitialised port
the initial state is $\pi_0$.

\begin{figure}

\begin{center}

\begin{picture}(250, 150)(0, -50)

\put(  0,   0){$\pi_0$}
\put(  0,  50){$\pi'_0$}
\put( 75,   0){$\pi_1$}
\put( 75,  50){$\pi'_1$}
\put(150,   0){$\pi_2$}
\put(200,   0){$\pi_3$}
\put(250,   0){$\pi_4$}

\put( 13, 3){\vector(1, 0){60}}
\put( 20, -10){$\query \tini$}

\put(  6, 10){\vector(0, 1){35}}
\put(-20, 24){$\query \tchg$}

\put( 13, 53){\vector(1, 0){60}}
\put( 20, 61){$\query \tini$}

\put( 88, 3){\vector(1, 0){60}}
\put(120, -10){$\pling \tchg$}

\put(213, 3){\vector(1, 0){35}}
\put(220, -10){$\pling \tini$}

\put( 72, 20){\oval(30, 30)[bl]}
\put( 57, 20){\vector(0, 1){10}}
\put( 57, 29){\line(0, 1){6}}
\put( 72, 35){\oval(30, 30)[tl]}
\put( 30, 24){$\query \tchg$}

\put( 88, 35){\oval(30, 30)[tr]}
\put(103, 35){\vector(0, -1){10}}
\put(103, 26){\line(0, -1){6}}
\put( 88, 20){\oval(30, 30)[br]}
\put(105, 24){$\pling \tquo$}

\put( 72, 70){\oval(30, 30)[l]}
\put( 72, 85){\vector(1, 0){10}}
\put( 82, 85){\line(1, 0){6}}
\put( 88, 70){\oval(30, 30)[r]}
\put( 65, 92){$\pling \tmes$}

\put( 72,-15){\oval(30, 30)[l]}
\put( 72,-30){\vector(1, 0){10}}
\put( 82,-30){\line(1, 0){6}}
\put( 88,-15){\oval(30, 30)[r]}
\put( 65,-43){$\pling \tmes$}

\put(171, 10){\oval(30, 30)[tl]}
\put(186, 10){\oval(30, 30)[tr]}
\put(171, 25){\vector(1, 0){10}}
\put(181, 25){\line(1, 0){5}}
\put(165,32){$\query \tquo$}

\put(171, -5){\oval(30, 30)[bl]}
\put(186, -5){\oval(30, 30)[br]}
\put(171, -20){\vector(1, 0){10}}
\put(181, -20){\line(1, 0){5}}
\put(165, -33){$\query \tchg$}

\end{picture}

\end{center}

\caption{\label{TPstat}$\mysymbol{Pstat}$ transition diagram (schematic)}

\end{figure}

     The equivalence between the set of traces defined by this
model and that defined by the composition of the three previous
models is formally established by the bisimulation:
\begin{displaymath}
\begin{array}{rcl}
\{ (\pi_0 & \mapsto & (\alpha_0, \beta_0, \gamma_0)) \\
(\pi'_0 (Q, Q^-) & \mapsto & (\alpha_0, \beta'_0 (Q^-), \gamma_1 (Q))) \\
(\pi_1 (E, Q) & \mapsto & (\alpha_1 (E), \beta_0, \gamma_1 (Q))) \\
(\pi'_1 (E, Q, Q^-) & \mapsto & (\alpha_1 (E), \beta'_0 (Q^-), \gamma_1 (Q))) \\
(\pi_2 (E, Q, P^+) & \mapsto & (\alpha_2 (E), \beta_1 (P^+), \gamma_1 (Q))) \\
(\pi_3 (E, Q, P^+) & \mapsto & (\alpha_2 (E), \beta_2 (P^+), \gamma_1 (Q))) \\
(\pi_4 & \mapsto & (\alpha_3, \beta_3, \gamma_1 (\any ))) \}
\end{array}
\end{displaymath}
(Proof that this relation is a bisimulation is omitted.  It follows by
straightforward application of the rule for composition of transition
models).

\end{document}

