Symbolic Observation Graph-Based Generation of Test Paths

sog-test-paths generates the observable paths from a Petri net model. It also generates the abstract paths.

Requirements

• A C++ compiler (gcc >= 9.3.0).

Compilation

The tool can be compiled as follow:

• First, run the make command inside the directory buddy22 in order to build the library used to manipulate Binary Decision Diagrams (BDD).

• Second, run make in the parser directory in order to build the library used to parse Petri net models from net files.

• Third, run the make command in the root directory to generate the executable file sog-test-paths.

Use

./sog-test-paths <command>

The following commands are available:

• To generate the reachability graph: use the option -r <filename.net>.
• To generate test paths covering the given observable transitions t1,t2,...,tn, use the option -o <filename.net> <output_file>.
• To generate test paths using structural analysis, use the option -a <filename.net>
• To generate the complete SOG corresponding to observable transitions, use the option -c <filename.net>