abcd.txt
13.4 KB
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
382
383
384
385
386
387
ABCD specification language
===========================
This document presents the ABCD language and compiler that is provided
with SNAKES.
WARNING: this documentation needs update since ABCD syntax has changed
a bit. A precise (but not user-friendly) syntax can be found in the
source:
- snakes/lang/abcd/abcd.pgen is the concrete grammar and
- snakes/lang/abcd/abcd.asdl is the abstract syntax
Introduction
------------
ABCD (Asynchronous Box Calculus with Data) is a specification language
whose semantics is given in terms of coloured Petri net. The formal
semantics will not be defined here, but only an intuition of it. ABCD
can be seen as both an Python based implementation and a variant of
several algebras of Petri nets:
- with respect to the versatile box calculus
(http://lacl.univ-paris12.fr/pommereau/publis/2007-dasd.html), ABCD
does not provide tasks and abort mechanism, but it allows nested
parallelism;
- with respect to the box calculus with coloured buffers or the box
calculus with high-level buffers
(http://lacl.univ-paris12.fr/pommereau/publis/2002-bcd.html and
http://lacl.univ-paris12.fr/pommereau/publis/2004-dads.html), ABCD
does not provide synchronous communication operations.
Syntax
------
The syntax of ABCD is a mix between Python and a process algebra. An
ABCD specification is structured as follows:
1. a possibly empty list of definitions, each being either
1. a Python ``def`` statement (function definition)
2. a Python ``import`` of ``from`` statement
3. an ABCD communication buffer definition
4. an ABCD sub-net definition (similar to a sub-program)
2. an ABCD process (similar to the ``main`` function of a C program)
Like in Python, block and sub-blocks are defined through indentation,
and comments begin with ``#`` and end with the line. Unlike Python,
scoping is lexical, with name masking as usual.
Python definitions
^^^^^^^^^^^^^^^^^^
Functions definitions and module imports are exactly as in Python.
Classes definition is not allowed, to do so, one must create a
separate Python module and import its content.
The following is an example of valid ABCD definitions:
from foo import *
from bar import spam
import math
def sqrt (x) :
return int(math.sqrt(x))
Buffers definitions
^^^^^^^^^^^^^^^^^^^
An ABCD buffer is implemented in the Petri nets semantics as a
coloured place, so a buffer is:
typed
values that can be inserted in the buffer must belong to a given
type; using ``object`` allows to put anything in the buffer.
unbounded
there is no a priori limit to the number of values that can be
inserted in a buffer, not even to the number of copies of a given
value within a buffer.
unordered
the order in which values are retrieved from a buffer is non
deterministic and is absolutely not related to the order of
insertion.
In order to contain the combinatorial explosion during the analysis of
the Petri net resulting from an ABCD specification, it is recommended
to take these aspects into account. In particular, it could be good
to:
- define buffer types as small as possible, allowing just the
expected values and no more;
- implement some policy in order to limit the number of values
simultaneously stored in a buffer. Anyway, if the buffer is
unbounded, it is likely that the resulting Petri net cannot be
analysed;
- implement a FIFO policy whenever possible, for instance by storing
numbered pairs ``(num, obj)`` instead of just ``obj`` and by
maintaining a counter for the next value to insert and the next to
get.
In order to declare a buffer, one has to write:
buffer NAME : TYPE = INIT
where ``NAME`` is the name of the buffer (a Python identifier),
``TYPE`` is its type (a Python type name or a more complex type
specification, see below), and ``INIT`` is the initial content of the
buffer: ``()`` if empty, or a comma separated list of values.
For instance, an empty buffer of integers and a buffer of strings with
two values can be declared as:
buffer count : int = ()
buffer messages : str = 'hello', 'world'
Buffer types can be:
Python classes
for instance ``int``, ``str``, ``float``, ``bool``, ``object``,
etc., including user defined classes.
Enumerated types
for instance ``enum(1, 3, 'foo', True)`` allows all the value listed
between the parenthesis but no other value.
Union types
for instance, ``int|float`` allows for integer as well as floating
point numbers. Intersection types, using operator ``&``, are also
allowed even if it hard to find a real usage for them.
Sets of typed values
for instance, ``{int|float}`` defines sets of numbers (integers or
floating point).
Lists of typed values
for instance, ``[str]`` defines lists of strings.
Dictionary types
for instance, ``str:int`` specifies ``dict`` objects whose keys
are strings and values are integers.
Cross product of types
for instance, ``(int, str)`` specifies tuples of length two whose
first item is an integer and second item is a string. Tuples of
length one *must* use a trailing comma; for instance, ``(int,)``
stands for integer singletons, but ``(int)`` is equivalent to just
``int`` as usual in Python.
Parentheses are allowed in order to combine complex types together, as
in ``(int|float):(str|NoneType)``.
Sub-nets definitions
^^^^^^^^^^^^^^^^^^^^
A sub-net is declared as follows:
net NAME (PARAMS) :
BLOCK
where ``NAME`` is the name of the sub-net (a Python identifier),
``PARAMS`` is a list of parameters (as in Python with default values
allowed but not ``*`` or ``**`` arguments) and BLOCK is an indented
block that follows the syntax of an ABCD specification (with optional
definitions and a mandatory process term).
Objects (Python functions or imports, and buffers) defined inside a
sub-net are local to it and cannot be accessed from the outside. But,
objects defined before the sub-net (unless nested in another sub-net)
are visible from within the sub-net and can be used.
Process terms
^^^^^^^^^^^^^
An ABCD process is defined as a term on a process algebra whose
operators are control flow operators:
sequential composition
the execution of ``A ; B`` starts with the execution of ``A``,
followed by the execution of ``B``
choice composition
the execution of ``A + B`` is either the execution of ``A`` or
that of ``B``, which is chosen non-deterministically.
loop composition
the execution of ``A * B`` starts by an arbitrary number of
executions of ``A``, followed by exactly one execution of ``B``,
the choice to loop or terminate is non-deterministic. So, ``A *
B`` is equivalent to ``B + (A ; B) + (A ; A ; B) + ...``.
parallel composition
the execution of ``A | B`` is that of both ``A`` and ``B``
concurrently.
Base terms of the algebra are either atomic processes or sub-net
instantiations. An atomic process, also called an action, is described
by a term enclosed in square brackets ``[...]``. The semantics of an
action is a Petri net transition. We distinguish:
``[True]``
the silent action that can always be executed and performs no
buffer access.
``[False]``
the deadlock action that can never be executed.
complex actions
such an action involve buffer accesses and an optional condition.
If ``expr`` denotes a Python expression, ``obj`` a Python constant
and ``var`` a Python identifier, buffer accesses may be:
- ``buffer+(expr)`` evaluated ``expr`` and adds the resulting value
to the buffer; this results in the semantics as an arc from the
transition to the buffer place, labeled by ``expr``.
- ``buffer-(obj)`` consumes the value ``obj`` from the buffer; this
results in the semantics as an arc from the buffer place to the
transition, labeled by ``obj``.
- ``buffer-(var)`` binds the variable ``var`` to a value present in
the buffer and consumes it; this results in the semantics as an arc
from the buffer place to the transition, labeled by ``var``.
- ``buffer?(obj)`` or ``buffer?(var)`` are similar except that they
just test the presence of a value but do not consume it; this is
semantically a read arc.
- ``buffer>>(var)`` consumes all the values in the buffer and bind
the resulting multiset to the variable ``var``; this is
semantically a flush arc.
- ``buffer<<(expr)`` evaluates the expression ``expr`` (the result
must be iterable) and adds all its values to the buffer; this is
semantically a fill arc.
For instance:
[count-(x), count+(x+1), shift?(j), buf+(j+x) if x<10]
This action can be execution if the following hold:
- buffer ``count`` must hold a value that it is bound to ``x``
- buffer ``shift`` mush hold a value that is bound to ``j``
- the type of buffer ``count`` must allow the value resulting from
the evaluation of ``x+1``
- the type of buffer ``buf`` must allow the value resulting from the
evaluation of ``j+x``
- expression ``x<10`` must evaluate to ``True``
If all these condition hold, the action can be executed, which results in:
- the chosen value for ``x`` is removed from buffer ``count``
- a new value corresponding to the evaluation of ``x+1` is added to
``count``
- a new value corresponding to the evaluation of ``j+x`` is added to
``buf``
This execution is atomic: it can be considered that all buffers accesses
and conditions evaluation are performed simultaneously and
instantaneously.
If ``count`` or ``shift`` contain more than one value, only those that
allow to fulfill the conditions listed above are considered. Among
those valuations, one is chosen non deterministically in order to
execute the action.
Note that the variables (like ``var``) used in an action do not need
to be declared and are local to this action. These are variables
exactly like in mathematics. Moreover, if a variable is used more than
once in an action, the execution gives it a single consistent value.
For instance, ``[count-(x), shit?(x) if x != 0]`` is executable only
if a same non-zero value can be found both in ``count`` and ``shift``.
Example
-------
Let's consider a simple railroad crossing involving:
- one track where trains can arrive repeatedly;
- one road crossing the track;
- a pair of gates that prevent cars to go on the track when a train
is approaching;
- a red light that prevent the train to cross the road before the
gates completely close.
When a train is approaching, the light is turned red and the gates are
asked to go down. When they arrive down, the light is reset to green.
When the train leaves the gates, they are asked to go up.
This system can be specified in ABCD as follows. We first specify
global buffers to model the red light and a communication channel
between trains and the gates:
# light is initially 'green'
buffer light : in('red', 'green') = 'green'
# no command is available initially
buffer command : in('up', 'down') = ()
Then we specify the behavior of the gates. We provide for it an
internal buffer allowing to easily observe its current state.
net gate () :
# gates are initially 'open'
buffer state : in('open', 'moving', 'closed') = 'open'
# a sequence of actions
# receive the command 'down' and start moving
([command-('down'), state-('open'), state+('moving')] ;
# finish to close and reset the light to 'green'
[state-('moving'), state+('closed'), light-('red'), light+('green')] ;
# receive the command 'up' and start moving
[command-('up'), state-('closed'), state+('moving')] ;
# finish to open
[state-('moving'), state+('open')])
# this sequence is infinitely repeated because the loop exit
# cannot be executed
* [False]
Then we specify the track on which trains can repeatedly arrive
net track () :
# we also need to observe trains position
buffer crossing : bool = False
# here also an sequence is infinitely repeated
# a train is approaching so the light is turned red and the
# gates are asked to close
([command+('down'), light-('green'), light+('red')] ;
# the train must wait for green light before to go further and
# cross the road
[light?('green'), crossing-(False), crossing+(True)] ;
# when the train leaves, gates are asked to open
[crossing-(True), crossing+(False), command+('up')])
* [False]
The full system is specified by running in parallel one instance of
the gates and one of the track.
gate() | track()
The Petri net from this specification can be drawn and saved to PNML
by invoking:
abcd --pnml railroad.pnml --dot railroad.png railroad.abcd
This creates both ``railroad.png`` and ``railroad.pnml``, the former
can be viewed in order to check how is the Petri net semantics, and
the latter can be used to verify the system. On such a small system,
SNAKES performs quickly enough for the verification. So we can use it
to iterate the marking graph and search for an insecure state, ie, in
which gates are open and train. The following program does the job:
from snakes.nets import *
n = loads(",railroad.pnml")
g = StateGraph(n)
for s in g :
m = g.net.get_marking()
if ("train().crossing" in m
and True in m["train().crossing"]
and "closed" not in m["gate().state"]) :
print s, m
print "checked", len(g), "states"
Here, no insecure marking is found. This would not be the case if we
would remove the red light since a train could always arrive on the
road faster than the gate could close.