Franck Pommereau

This release introduces a first version of a graphical ABCD simulator. Invoking command abcd with option --simul yields a window in which you may execute your ABCD code interactively, going back and forth into the trace executed so far. The top-right panel shows the source code, with the currently executable actions highlighted. The top-left panel shows all the currently executable actions with their modes. Here, we have selected one of the modes of the odd() net action, so it is highlighted in green. The bottom-right panel shows the current state of buffers. Finally the bottom-left panel shows the current trace; clicking on an action in this trace puts the other panels into the states corresponding to when the action had just been executed. (A special action allows to observe the initial state.) Using the buttons on the middle-left, you may execute a selected action, remove the last action from the trace, or resume simulation when you are done with trace inspection (which selects the last obtained state).

Moreover, a reachability checker has been introduced also. It is still very suboptimal since it computes the reachability graph by directly using SNAKES firing, future version will improve efficiency using model compilation and introduce CTL* model-checking. Right now, to check properties, just insert assertions at the very end of your ABCD spec, for instance assert 5 not in _["buff"] allows to check that no token whose value is 5 is ever inserted into buffer buff, where _ is simply a Marking object and "buff" is a buffer name (including the instance path for buffers nested into nets, just as show in the bottom-right panel of the simulator). Then, using option --check, the state space of the Petri net corresponding to the ABCD model is computed and each assertion is checked against every reachable state. Whenever a state that violates an assertion is reached, a trace from the initial state to this error state is printed and the analysis stops immediately. If you combine --check with --simul, such an error trace is displayed in the simulator instead of on your terminal.

Finally, this release fixes several bugs, in particular a blocking bug on transitions firing that appeared with the latests releases of Python.

As usual, you may download the source code or install the Ubuntu package.