
%\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{\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{\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{Deriving the Big Predicate}

\subsection{User Messages}

\begin{linpar}
$Q.P^O.\tmes (u, H)$ \\
$Q.P^I.\tmes (u, H)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$P$ \> = port associated with channel end $\function{from} (H)$. \\
$Q$ \> = port associated with channel end $\function{to} (H)$. \\
$u$ \> = user field transferred in message. \\
$H$ \> = data transfer half-channel.
\end{tabbing}

$\mysymbol{mes}$ output is in the alphabets of 
port $P$, the user process, and the message delivery system.
$\mysymbol{mes}$ input is in the alphabets of port $Q$,
the user process, and the message delivery system.
\end{description}
\end{linpar}

\subsection{Control Transfer Messages}

     The $\mysymbol{ini}$ message is sent from a port process
to its successor on termination of the former.  It carries information
needed to initialise the new port. \\ \\
\begin{linpar}
$P.S^O.\tini (E, Q, u, H)$ \\
$P.S^I.\tini (E, Q, u, H)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$P$ \> = port formerly associated with channel end $E$. \\
$S$ \> = successor port to $P$. \\
$E$ \> = a channel end. \\
$u$ \> = user field transferred in message. \\
$H$ \> = access transfer half-channel.
\end{tabbing}
$\mysymbol{ini}$ output is in the alphabets of the user process,
port $P$, and the message delivery system.
$\mysymbol{ini}$ input is in the alphabets of the user process,
port $S$, and the message delivery system.
\end{description}
\end{linpar}

\subsection{Port Repointing Messages}

These messages are used during transfer of access to a channel end
to inform the port associated with the {\em partner} channel end
of the move. $\tquo$ is an acknowledgement of a $\tchg$ message.\\ \\
\begin{linpar}
$Q.P^O.\tchg (E, S, H)$ \\
$Q.P^I.\tchg (E, S, H)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$P$ \> = port formerly associated with channel end $E$. \\
$Q$ \> = port associated with partner of $E$. \\
$S$ \> = successor port to $P$. \\
$E$ \> = a channel end. \\
$H$ \> = access transfer half-channel.
\end{tabbing}
$\mysymbol{chg}$ output is in the alphabets of the user process,
port $P$, and the message delivery system.
$\mysymbol{chg}$ input is in the alphabets of port $Q$ and
the message delivery system.
\end{description}
\end{linpar}
\ \\ \\
\noindent
\begin{linpar}
$P.Q^O.\tquo (E, H)$ \\
$P.Q^I.\tquo (E, H)$ 

\begin{description}
\item[]
\begin{tabbing}
$P$  \=\kill
$P$ \> = port formerly associated with channel end $E$. \\
$Q$ \> = port associated with partner of $E$. \\
$E$ \> = a channel end. \\
$H$ \> = access transfer half-channel.
\end{tabbing}
$\mysymbol{quo}$ output is in the alphabets of 
port $Q$, and the message delivery system.
$\mysymbol{quo}$ input is in the alphabets of port $P$ and
the message delivery system.
\end{description}
\end{linpar}

\section{The Port Process}

     A port process 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.

\begin{linpar}
     The alphabet of a port process $P$ contains \\ \\
Main control thread events

\begin{description}
\item[]
\begin{tabbing}
$P.\any^I.\tini \any$ \\
$\any.P^O.\tini \any$
\end{tabbing}
\end{description}

Repointing events

\begin{description}
\item[]
\begin{tabbing}
$P.\any^I.\tchg \any$ \\
$\any.P^O.\tquo \any$ \\
$\any.P^O.\tchg \any$ \\
$P.\any^I.\tquo \any$
\end{tabbing}
\end{description}

Communication events

\begin{description}
\item[]
\begin{tabbing}
$\any.P^O.\tmes \any$ \\
$P.\any^I.\tmes \any$
\end{tabbing}
\end{description}
\end{linpar}
\  \\ \\
The traces of $P$ satisfy
\begin{enumerate}
\item
The trace restricted to $\tmes$, $\tchg$, $\tquo$ and $\tini$ output events,
and $\tini$ inputs, is a prefix of some sequence from
\begin{description}
\item[]
\begin{tabbing}
$\cal{S} (E) $
\end{tabbing}
\end{description}
if $P$ is an initialised port, or
\begin{description}
\item[]
\begin{tabbing}
$ \bigcup_E 
\{ \langle P.\any^I.\tini (E, \any, \any, \any) \rangle \} \cal {S} (E) $
\end{tabbing}
\end{description}
if it is uninitialised.  Here
\begin{eqnarray*}
\cal{S} (E) & = &
\{\langle \any.P^O.\tmes (\any, \function{from} (E)) \rangle,
\langle \any.P^O.\tquo \any \rangle\}^N \\ &&
\{ \langle \any.P^O.\tchg (E, \any, \any) \next
\any.P^O.\tini (E, \any, \any, \any) \rangle \}
\end{eqnarray*}
\item
The trace restricted to repointing events and $\tini$ output is a prefix of
a sequence from
\begin{description}
\item[]
\begin{tabbing}
$
\{ \langle
P.Q^I.\tchg (F, \any, \any) \next Q.P^O.\tquo (F)
\rangle
%\suchthat F \in \mysymbol{Ends}, Q \in \mysymbol{Ports}
\}^N $ \\
$\bigcup_{R, H}
\{ \langle \any.P^O.\tchg (\any, R, H) \rangle \} $
$\{ \langle P.\any^I.\tquo \any \rangle ,
\langle P.\any^I.\tchg \any \rangle \} $ \\ \ \ \ \ \ \
$\{ \langle R.P^O.\tini (\any, \any, \any, H) \rangle \}$
\end{tabbing}
\end{description}

\item
In any event from
\nopagebreak
\begin{description}
\item[]
\begin{tabbing}
$Q.P^O.\tmes \any$ \\
$Q.P^O.\tchg \any$ \\
$\any.P^O.\tini (\any, Q, \any, \any)$
\end{tabbing}
\end{description}
appearing in a trace, the $Q$ field must have the same value as the
$Q$ field in the most recent preceding event of type
\begin{description}
\item[]
\begin{tabbing}
$P.\any^I.\tchg (\any, Q, \any)$
\end{tabbing}
\end{description}
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)
\begin{description}
\item[]
\begin{tabbing}
$P.\any^I.\tini (\any, Q, \any, \any)$
\end{tabbing}
\end{description}
event (if it is uninitialised).  These constraints impose that communications 
are always sent to the active partner port.

\end{enumerate}
(These constraints describe a non-terminating process, because they don't
restrict occurrences of message input.)

\end{document}
