Introduction

The modsog module implements construction algorithms for the Symbolic Observation Graph (SOG).

A complete version of the tool is also available as a unix-command terminal mode.

Using modsog via the GUI

The CPN-AMI platform GUI provides access via menus to the modular SOG construction. The net modules should first be entered via the graphical editor and syntax-checked.

Let us have a look on its use for a given model (see below). Blue transitions correspond to interfaces (i.e. transitions shared with the environment).

Once all modules are entered and syntax-checked, the modular construction is provided via the CPN-AMI interface, in a dedicated menu.

Then you are required to enter a formula to be verified in a dedicated window. Enter first the modules names, then, the interface transitions (shared transitions) of each module, and finally, teh transitions occuring in teh formula. The fomat described in the following window must be respected.

Statistics about the modular SOG construction are then displayed in the result window

Using modsog as command line

You may also use modsog outside of CPN-AMI, which is useful for scripting purposes. Then, you must extract the executable file inside the CPN-AMI package and then feed it with PROD format

Expected input

• menu 1: a single net file in the prod format ;
• menu 2: a single net file in the prod format, a text file containing the number and names of the transitions appearing in the LTL\X formula to be checked with the SOG technique, and the (expected) place-bound for the Petri net ;
• menu 3: a list of files pairs, the first file being a prod net and the second a text file containing the number and names of the interface transitions (shared by the net file and its environment), followed by a file with the transitions of the formula (as for menu 2).

Menu 1

The syntax of the command is:

modsog file.net

This option constructs and provides information about the BDD representation of the state space: number of BDD nodes and number of reachable markings.

For the example provided in the package, use:

modsog ex_modsog.net

Menu 2

modsog file.net formula_trans bound

This option constructs the SOG for the net w.r.t. the observed transitions given in the formula_trans file. It outputs:

• statistics on the graph construction ;
• the size of the SOG (number of nodes and arcs) ;
• upon user request, the final number of BDD nodes and the detailled graph structure.

modsog ex_modsog.net formula_trans 1

Menu 3

The syntax of the command is:

modsog file_1.net interface_1 ... file_n.net interface_n formula_trans

This option constructs on-the-fly the synchronous product of the nets modules SOGs w.r.t. the observed transitions given in the formula_trans file, as well as the transitions occurring in the interface files (interface_1...interface_n). It outputs:

• statistics on the synchronous product graph construction ;
• the size of the modular SOG (number of nodes and arcs) ;
• upon user request, the final number of BDD nodes and the detailled graph structure.

For the example provided in the package, use:

modsog ex_modsog_1.net ex_interface_modsog_1 ex_modsog2.net ex_interface_modsog_2 formula_trans