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:

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:

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.