summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/zed-csp/csp2e.tex
blob: 880eedf08fea4fc6be1d0a7dfb3dc0e02fc5ccf4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
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}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%