From e0c6872cf40896c7be36b11dcc744620f10adf1d Mon Sep 17 00:00:00 2001
From: Norbert Preining <norbert@preining.info>
Date: Mon, 2 Sep 2019 13:46:59 +0900
Subject: Initial commit

---
 macros/latex/contrib/zed-csp/csp2e.tex | 381 +++++++++++++++++++++++++++++++++
 1 file changed, 381 insertions(+)
 create mode 100644 macros/latex/contrib/zed-csp/csp2e.tex

(limited to 'macros/latex/contrib/zed-csp/csp2e.tex')

diff --git a/macros/latex/contrib/zed-csp/csp2e.tex b/macros/latex/contrib/zed-csp/csp2e.tex
new file mode 100644
index 0000000000..880eedf08f
--- /dev/null
+++ b/macros/latex/contrib/zed-csp/csp2e.tex
@@ -0,0 +1,381 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%       csp2e.tex               ->      hack guide to zed-csp.sty 
+
+%       (c) Jim Davies September 1994  >> Version 0 <<
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\documentclass[12pt]{article}
+
+% \usepackage[yy]{lucbr} 
+
+% Uncomment the above line if you have the Lucida fonts and want to
+% use them to set csp.  Note that you may have to change the [yy]
+% option if you are not using the Y&Y font naming convention. 
+
+\usepackage{zed-csp}
+
+\advance\textwidth 30mm
+\advance\oddsidemargin -15mm 
+\advance\evensidemargin -15mm 
+\advance\textheight 35mm
+\advance\topmargin -20mm
+
+\begin{document} \thispagestyle{empty}
+
+\def\AMS{%
+   $\cal{A}$
+   \kern-.5em\lower.5ex\hbox{$\cal{M}$}\kern-.125em$\cal{S}$}
+
+\parindent 0pt
+\parskip 10pt
+
+{\huge\bf Setting real-time CSP}
+
+\vskip 2mm
+
+{\Large Jim Davies}
+
+\vskip 8mm
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Introduction}
+
+The language and models of CSP have undergone a gradual evolution
+since the publication of the first CSP textbook---Hoare's {\sl
+Communicating Sequential Processes\/} (Prentice-Hall, 1985).  The
+forthcoming text on real-time CSP will provide for some
+degree of standardisation.  
+
+In parallel, we hope to provide a standard set of macros for setting
+documents which use CSP notation.  This will allow users to exchange
+documents in electronic form, and will form part of the user interface
+to the language tools.
+
+The macros are defined by a style file called \verb|zed-csp.sty|.
+This should work with \LaTeXe.  Inquiries, suggestions, or complaints
+should be addressed to 
+
+\begin{center}
+  {\tt Jim.Davies@comlab.ox.ac.uk}.
+\end{center}
+
+Note that this is a fairly quick fix of the style to enable myself and
+others to use the improved facilities offered by the new version of
+\LaTeX.  It has not been rigorously tested, although it seems to work
+for me.  
+
+\section{Symbols}
+
+We can divide the symbols used into three separate classes: symbols
+for the language itself, symbols used in the definition of the
+semantics, and symbols used in the specification language.  
+
+\subsection{The language of real-time CSP}
+
+The operators of real-time CSP are set using macros of the same name.
+The macros for atomic operators begin with an uppercase letter; the
+same is true for those representing indexed versions of parallel and
+choice operators.  All other macros are lowercase throughout.  Some
+operators accept optional arguments, but no argument is compulsory.
+
+When an operator with an optional argument appears within an optional
+argument, \LaTeX may require assistance if it is to parse the
+expression correctly.  In these circumstances, we use an extra pair of
+braces to delimit the process expression: e.g., 
+\begin{center}
+  \verb|\Ftf[{P \parallel[A] Q}]|.
+\end{center}
+
+\begin{tabular}{p{2in}p{1.5in}c} \\ \\
+bottom          & \verb|\Bottom|        & $ \Bottom  $  \\[1ex]
+stop            & \verb|\Stop|          & $ \Stop    $  \\[1ex]
+skip            & \verb|\Skip|          & $ \Skip    $  \\[1ex]
+wait            & \verb|\Wait|          & $ \Wait $     \\[1ex]
+prefix          & \verb|\then|          & $ \then $     \\[1ex]
+external choice & \verb|\extchoice|     & $ \extchoice $ \\[1ex]
+internal choice & \verb|\intchoice|     & $ \intchoice $ \\[1ex]
+hiding          & \verb|\hide|          & $ \hide $ \\[1ex]
+parallel        & \verb|\parallel[A][B]|& $ \parallel[A][B] $\\[1ex]
+interleaving    & \verb|\interleave|    & $ \interleave $ \\[1ex]
+sharing         & \verb|\parallel[C]|   & $ \parallel[C] $ \\[1ex]
+recursion       & \verb|\mu X \spot P|  & $ \mu X \spot P $ \\[1ex]
+timeout         & \verb|\timeout[t]|    & $\timeout[t]$\\[1ex]
+transfer        & \verb|\transfer[t]|   & $\transfer[t]$\\[1ex]
+interrupt       & \verb|\interrupt|     & $\interrupt$ \\[1ex]
+timer           & \verb|\at|            & $\at$ \\[1ex]
+indexed external choice & \verb|\Extchoice| & $ \Extchoice $ \\[1ex]
+indexed internal choice & \verb|\Intchoice| & $ \Intchoice $ \\[1ex]
+indexed alphabet parallel & \verb|\Parallel| & $ \Parallel $ \\[1ex]
+indexed interleaving & \verb|\Interleave| & $ \Interleave $
+\end{tabular}
+
+\subsection{Parallel combinations}
+
+There are several ways to denote the parallel combination of
+two processes in CSP.  Firstly, we can describe the set of events upon
+which they must cooperate: e.g., in the process
+\[
+P \parallel[C] Q
+\]
+components $P$ and $Q$ must cooperate upon every event from the shared
+set $C$.  Alternatively, we can declare two alphabets
+\begin{eqnarray*}
+\alpha P & = & A \\
+\alpha Q & = & B
+\end{eqnarray*}
+and write
+\[
+P \parallel Q
+\]
+to denote the parallel combination in which $P$ and $Q$ must cooperate
+upon every event in the intersection of their alphabets.  Finally, we
+can add explicit alphabet information to the parallel operator: e.g.,
+\[
+P \parallel[A][B] Q
+\]
+is equivalent to the above parallel combination, given the values
+chosen for $\alpha P$ and $\alpha Q$.
+
+\subsection{Delays and timers}
+
+We write $\Wait t ; P$ to denote the process which will delay for time
+$t$ before behaving as $P$.  The wait process is a delayed form of
+termination $\Skip$: i.e.,
+\begin{eqnarray*}
+\Wait 0 & = & \Skip
+\end{eqnarray*}
+To model a nondeterministic delay, we can use an internal choice
+operator indexed by a range of time values:
+\[
+\Intchoice_{t \in [t_1,t_2)} \Wait t
+\]
+A convenient abbreviation for this involves overloading the $\Wait$
+operator: e.g.,
+\[
+\Wait [t_1,t_2)
+\]
+abbreviates the above choice.
+
+External events in a process description are performed in cooperation
+with the environment of that process.  It is therefore quite likely
+that an external event will not occur as soon as the process is ready.
+The time elapsed between the offer of an event and its occurrence can
+influence future behaviour; the rest of the process description should
+be allowed to refer to this time.
+
+Accordingly, real-time CSP includes a timer construct, or
+`passage-of-time' operator.  We write
+\[
+a \at t \then P \qquad \qquad \hbox{\verb|a \at t \then P|}
+\]
+to denote a process which is initially ready to engage in event $a$.
+The time variable $t$ is assigned the relative time at which $a$
+occurs.  This is the same as the elapsed time between control being
+passed to this process---at which point the offer of $a$ is made---and
+the event $a$ actually occuring.
+
+A useful extension to this, which adds nothing to the expressivity of
+the language but can make for more intelligible process descriptions,
+is the offer timeout.  We write
+\[
+a \at t \{ d \} \then P \qquad \qquad
+\hbox{\verb|a \at t \{ d \} \then P|}
+\]
+to denote a process which offers to perform $a$, and will store the
+time of occurrence in $t$, but will withdraw the offer if it has not
+been accepted by time $d$.  (This form of timeout was suggested
+by Guy Leduc for his version of timed LOTOS.)
+
+\section{Mathematical language}
+
+The semantic models of CSP come with a great deal of notational
+baggage.  We need to define operators to project information out of
+traces, refusals, and timed failures.  There is also a specification
+language based upon the timed semantics, and the names used for the
+models themselves.
+
+\subsection{Logic, sets, and sequences}
+
+\begin{tabular}{c@{\hspace{0.55in}}c@{\hspace{0.55in}}c} \\
+\begin{tabular}[t]{@{}lc}
+\verb|\defs| & $ \defs $ \\[0.6ex]
+\verb|\mu| &  $ \mu $ \\[0.6ex]
+\verb|\lambda| & $ \lambda $ \\[0.6ex]
+\verb|\exists| &  $ \exists $ \\[0.6ex]
+\verb|\forall| &  $ \forall $ \\[0.6ex]
+\verb|\spot| &  $ \spot $ \\[0.6ex]
+\verb|\nat| &  $ \nat $ \\[0.6ex]
+\verb|\num| & $ \num $ \\[0.6ex]
+\verb|\rat| & $ \rat $ \\[0.6ex]
+\verb|\real| & $ \real $ \\[0.6ex]
+\verb|\seq| & $ \seq $
+\end{tabular} &
+\begin{tabular}[t]{lc}
+\verb|\land| &  $ \land $ \\[0.6ex]
+\verb|\lor| &  $ \lor $ \\[0.6ex]
+\verb|\Land| & $ \Land $ \\[0.6ex]
+\verb|\Lor| & $ \Lor $ \\[0.6ex]
+\verb|\lnot| &  $\lnot $ \\[0.6ex]
+\verb|\implies| & $ \implies $ \\[0.6ex]
+\verb|\iff| &  $ \iff $ \\[0.6ex]
+\verb|\upto| & $\upto$ \\[0.6ex]
+\verb|\le| & $ \le $ \\[0.6ex]
+\verb|\ge| & $ \ge $ \\[0.6ex]
+\verb|\project| & $ \project $
+\end{tabular} &
+\begin{tabular}[t]{lc}
+\verb|\power| &  $ \power  $ \\[0.6ex]
+\verb|\finset| & $ \finset $ \\[0.6ex]
+\verb|\cross| &  $ \cross $ \\[0.6ex]
+\verb|\union| & $ \union $ \\[0.6ex]
+\verb|\inter| & $ \inter $ \\[0.6ex]
+\verb|\Union| & $ \Union $ \\[0.6ex]
+\verb|\Inter| & $ \Inter $ \\[0.6ex]
+\verb|\dom| & $ \dom$ \\[0.6ex]
+\verb|\ran| & $ \ran$ \\[0.6ex]
+\verb|\emptyset| & $\emptyset$ \\[0.6ex]
+\verb|\set{x}| & $ \set{x} $
+\end{tabular}
+\end{tabular}
+
+\subsection{Operators on traces}
+
+\begin{tabular}{p{1.95in}p{1.75in}c} \\
+empty trace     & \verb|\nil|           & $\nil $ \\[0.6ex]
+trace   & \verb|\trace{e_1,e_2}|        & $\trace{e_1,e_2}$\\[0.6ex]
+catenation of traces & \verb|\cat|      & $\cat $ \\[0.6ex]
+count           & \verb|\cnt|           & $\cnt $ \\[0.6ex]
+during          & \verb|\during|        & $\during $ \\[0.6ex]
+tick event      & \verb|\tick|          & $\tick$ \\[0.6ex]
+subsequence     & \verb|\subseq|        & $\subseq$ \\[0.6ex]
+data values     & \verb|\data|          & $\data$ 
+\end{tabular}
+
+\subsection{Projection functions}
+
+\begin{tabular}{p{1.95in}p{1.75in}l} \\
+  begin         & \verb|\Begin    |  & $\Begin$   \\[0.4ex]
+  end           & \verb|\End      |  & $\End  $   \\[0.4ex]
+  head          & \verb|\Head     |  & $\Head $   \\[0.4ex]
+  first         & \verb|\First    |  & $\First$   \\[0.4ex]
+  tail          & \verb|\Tail     |  & $\Tail $   \\[0.4ex]
+  front         & \verb|\Front    |  & $\Front$   \\[0.4ex]
+  last          & \verb|\Last     |  & $\Last $   \\[0.4ex]
+  times         & \verb|\Times    |  & $\Times$   \\[0.4ex]
+  events        & \verb|\Events   |  & $\Events$  \\[0.4ex]
+\end{tabular}
+
+$\Times$ and $\Events$ are projection functions from timed traces to
+sequences of times and sequences of events respectively.  $\Head$ and
+$\Tail$ may be applied to any sequence.  $\Begin$ and $\End$ may be
+applied to timed traces and timed refusals.  $\First$ is a synonym for
+$\Head$. $\Front$ is the dual of $\Tail$.  $\Last$ is the dual of
+$\Head$.
+
+To denote the set of events mentioned in a timed or untimed trace or
+refusal, we prefix the name of the object with $\alpha$.  For example,
+the set of events mentioned in the timed trace $s$ would be written
+$\alpha s$.  Earlier version of real-time CSP did this using the
+$\sigma$ operator to avoid confusion with process alphabets.  Where
+there is scope for confusion, we suggest that this practice is
+continued.
+
+\subsection{Semantic functions, models, and spaces}
+
+In {\sl  Advanced CSP}, we use long names for the semantic functions:
+
+\begin{tabular}{p{1.95in}p{1.75in}l} \\
+semantics       & \verb|\Semantics|     & $\Semantics$ \\
+traces          & \verb|\Traces|        & $\Traces$ \\
+failures        & \verb|\Failures|      & $\Failures$ \\
+timed failures  & \verb|\TimedFailures| & $\TimedFailures$ \\
+divergences     & \verb|\Divergences|   & $\Divergences$ \\
+infinites       & \verb|\Infinites|     & $\Infinites$
+\end{tabular} 
+
+Any semantic function macro can be given an optional argument. This
+will be set within semantic brackets: e.g., \verb|\Traces[P]| yields
+$\Traces[P]$.  To obtain the semantic brackets alone, use the
+\verb|\semb| macro; this takes a single compulsory argument.
+Alternatively, the macros \verb|\leftsemb| and \verb|\rightsemb|
+produce left and right semantic brackets respectively.
+
+In theoretical papers, we often need to refer to several models,
+functions, and associated spaces.  To make things easier on ourselves,
+we adopt short names for these mathematical objects, using subscripts
+to identify the model concerned.  For example, the objects associated
+with the timed failures model are all subscripted with $TF$.
+
+The models themselves have macros beginning \verb|\M|:
+
+\begin{tabular}{p{2.4in}p{1.1in}l} \\
+traces                          & \verb|\Mut|   & $ \Mut  $     \\
+failures                        & \verb|\Muf|   & $ \Muf  $     \\
+failures-divergences            & \verb|\Mufd|  & $ \Mufd $     \\
+timed failures                  & \verb|\Mtf|   & $ \Mtf  $     \\
+timed failures-stability        & \verb|\Mtfs|  & $ \Mtfs $     \\
+timed infinite                  & \verb|\Mti|   & $ \Mti  $
+\end{tabular} 
+
+The matching semantic functions use \verb|\F| instead---e.g.,
+\verb|\Fut| for untimed traces---and the observation spaces use
+\verb|\S|.  
+
+\subsection{Refinement and satisfaction}
+
+The satisfaction notation employed in Hoare's {\sl Communicating
+Sequential Processes} has been retained.  We also have a refinement
+relation between processes, possibly indexed by the name of the model
+concerned.
+
+The satisfaction relation is set as follows: \verb|P \sat S| produces
+$P \sat S$.  The refinement relation is produced by \verb|\lessdet| (or
+\verb|refinedby|, a synonymbol).  
+
+\subsection{Specifications}
+
+To capture timing constraints at the level of the semantic models, we
+use a number of specification `macros'.  These are set using \LaTeX\
+macros which begin with an `m' (for macro) and are then capitalised.
+\par 
+\begin{tabular}{p{1.95in}p{1.75in}l} \\
+internal        & \verb|\mInternal  | & $ \mInternal $    \\[0.4ex]
+refuses         & \verb|\mRef       | & $ \mRef      $    \\[0.4ex]
+at              & \verb|\mAt        | & $ \mAt       $    \\[0.4ex]
+live            & \verb|\mLive      | & $ \mLive     $    \\[0.4ex]
+open            & \verb|\mOpen      | & $ \mOpen     $    \\[0.4ex]
+from            & \verb|\mFrom      | & $ \mFrom     $    \\[0.4ex]
+until           & \verb|\mUntil     | & $ \mUntil    $    \\[0.4ex]
+live from       & \verb|\mLiveFrom  | & $ \mLiveFrom  $   \\[0.4ex]
+open from       & \verb|\mOpenFrom  | & $ \mOpenFrom  $   \\[0.4ex]
+name of last    & \verb|\mNameOfLast| & $ \mNameOfLast $  \\[0.4ex]
+before          & \verb|\mBefore    | & $ \mBefore   $    \\[0.4ex]
+after           & \verb|\mAfter     | & $ \mAfter   $     \\[0.4ex]
+time of last    & \verb|\mTimeOfLast| & $ \mTimeOfLast $  \\[0.4ex]
+\end{tabular}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Discussion}
+
+\subsection{Dependencies}
+
+You must have the AMS fonts available, and the {\tt amsfonts}
+installation must have been performed for \LaTeXe.  This requires the
+{\tt mfnfss} package; it takes about twenty seconds. 
+
+\subsection{CSP and Z}
+
+You may have problems if you try to use the {\tt zed-csp} package with
+{\tt fuzz} or any style package that uses the AMS fonts.  The good
+news is that you shouldn't need them.  All of the AMS symbols are
+defined in the {\tt zed-csp} package, using the standard names.  
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-- 
cgit v1.2.3

