ABCD is a modelling language that brings together process algebras and Python programming with a Petri net semantics. A compiler for ABCD is shipped with SNAKES, a description of the language and its semantics can be found in my habilitation thesis (section 3.3). On the other hand, Neco, with the help of SPOT, is able to perform efficient LTL model-checking of Petri-nets and, in particular, it accepts ABCD models as its input.
In this post we look at a concrete example of how to use Neco to model-check the ABCD model of a railroad crossing system. A basic knowledge of ABCD and LTL is required to fully understand this post.
First of all, note that not all features of ABCD are supported by Neco, in particular:
- in LTL formulas, places names cannot have dots or parentheses, so if we declare an ABCD buffer within a net sub-process, the corresponding place will not be usable. For this reason, the buffers used in the formulas shall be global;
- symbols and enumerated types are not supported by Neco, so we'll use integers and dedicated constants to model the various symbols of the system.
As usual, the railroad system is composed of a pair of gates, a number of tracks equipped with green/red lights to control the progression of the trains, and a controller that counts the trains and operate the gates appropriately. These components communicate through various channels.
The ABCD model starts with global definitions: constants as just
explained, and various buffers. Sorry for the syntax highlight below
which is for Python and does not handle ABCD keywords. Buffer green
stores the number of each track that has a green light, so a red light
is modelled by the absence of the corresponding token. Other buffers
are dedicated to the communication between the components: enter
receives the track numbers on which a train approaches the gates;
leave
receives the track numbers on which a train leaves the gates;
down
allows to ask the gates to go down; up
allows to ask the
gates to go up; done
is used by the gates to inform the controller
when they have finished a command.
# number of tracks
const NUM = 2
# the states of the gates
const OPEN = 42
const MOVING = 43
const CLOSED = 44
# green lights on the tracks
buffer green : int = range(NUM)
# tracks -> controller
buffer enter : int = ()
buffer leave : int = ()
# controller -> gates
buffer down : BlackToken = ()
buffer up : BlackToken = ()
# gates -> controller
buffer done : int = ()
The gates are modelled with a net sub-process and a buffer state
reflecting the current position of the gates. The associated process
is a simple sequence of four actions repeated infinitely often: wait
for the request to go down and start proceed it; arrive down and
notify the controller; wait for the request to go up and start proceed
it; arrive up and notify the controller.
# current state of the gates, initially OPEN
buffer state : int = OPEN
net gates () :
([down-(dot), state<>(OPEN=MOVING)] ;
[state<>(MOVING=CLOSED), done+(CLOSED)] ;
[up-(dot), state<>(CLOSED=MOVING)] ;
[state<>(MOVING=OPEN), done+(OPEN)])
* [False]
The model for the tracks has the same structure. A local buffer
crossing
is marked when a train is crossing the road and a series of
actions executed repeatedly corresponds to the successive steps of the
progression of a train: approach the gates and switch the green light
to red; start crossing the road only on a green light and switch it to
red again; leave the crossing zone.
buffer crossing : int = ()
net track (this) :
([enter+(this), green-(this)] ;
[green-(this), crossing+(this)] ;
[crossing-(this), leave+(this)])
* [False]
Then, the model for the controller is composed of one buffer count
to count the trains present in the supervised zone, one buffer
waiting
to record on which track a train is waiting for the green
light, and one process that can repeatedly execute one of four
behaviours:
- detect the first train approaching (guard
c == 0
) and ask the gates to go down, then wait until they arrive down and give the green light to the train that triggered this behaviour; - count another train approaching and give it the green light (
c > 0
); - count a train leaving the zone while there are still other trains
in the zone (
c > 1
); - detect that the last train leaves the zone (
c == 1
), ask the gates to go up and wait until this order is executed. When a train leaves, the corresponding light is turned green again so another train is allowed to approach on this track. Without such a mechanism, we could have an accumulation of tokens in bufferleave
.
net controller () :
buffer count : int = 0
buffer waiting : int = ()
(([enter-(num), count<>(c=c+1), down+(dot), waiting+(num) if c == 0]
; [done-(CLOSED), waiting-(num), green+(num)])
+ [enter-(num), count<>(c=c+1), green+(num) if c > 0]
+ [leave-(num), green+(num), count<>(c=c-1) if c > 1]
+ ([leave-(num), waiting+(num), count<>(c=c-1), up+(dot) if c == 1]
; [done-(OPEN), waiting-(num), green+(num)]))
* [False]
The complete system is just a parallel composition of instances of these nets: one pair of gates, one controller and several tracks.
# all components in parallel
gates() | controller() | track(0) | track(1)
All this is saved in a file railroad.abcd
that can
be fed to Neco in order to compile it as an optimised library:
$ neco-compile -lcython --abcd railroad.abcd
Option -lcython
allows to target the Cython backend of Neco that is
compiled to C++ and then to machine code (instead of Python code which
is the default), yielding a file net.so
. Then, we compile the
formula we want to check on the model:
$ neco-check --formula="G (marking(crossing) >= [0] => marking(state) = [44])"
That can be translated as: in every reachable state, if a train is
crossing the gates on track 0 (so, 0 is in the marking of buffer
crossing
), then the gates must be closed (so, the marking of buffer
state
is just the value 44). This formula is also compiled to
machine code producing a file checker.so
as well as a file
neco_formula
that is an abstracted version of our formula that is
latter passed to SPOT and is visible in the output of neco-spot
.
Finally, we launch the model-checker with:
$ neco-spot neco_formula
Formula: (G ((p0) => (p1)))
...
no counterexample found
The last line shows that the model is correct with respect to our
formula. We can check a similar formula for track 1, and we can also
check that the gate do not stay closed forever using formula G
((marking(state) = [44]) => F (marking(state) = [42]))
that can be
read as: in every reachable state, if the gates are closed, then in a
future state, gates are open.