Graphgen
Graphgen
Graphgen is a command line tool written in Java for state space analysis of Time-Basic (TB) Petri nets, a powerful formalism for real-time systems where time constraints are expressed as intervals,representing possible transition firing times, whose bounds are functions of marking’s time description.
Graphgen build a symbolic reachability graph relying on a sort of time coverage, and overcomes the limitations of the only available analyzer for TB nets, based in turn on a time-bounded inspection of a (possibly infinite) reachability tree.
Presentation
Parallel and Distributed versions
The major weakness of the state space exploration approach is that the size of the state space grows exponentially in the size of the model and this creates the state space explosion problem. Our approach does not alleviate this problem, but it increases the memory available for storage of the state space, and has the potential for a speed-up in time. We based on a simpe basic idea: We could use different computational units to perform the analysis and build different partitions of the reachability graph in parallel with the aim at reducing the amount of time required by a sequential computation and increasing the number of real-sized analyzable systems.
We implements a version of Graphgen analysis tool for the following computational models:
Getting Started
• Graphgen - sequential version (graphgen.jar)
After downloading the jar file from above, you are able to test Graphgen by simple typing:
To watch Graphgen in action, you can run it with the following TB nets examples:
• Producer/Consumer producer_consumer.xml
• The Gas Burner (0,5) gas05.xml
• The Gas Burner (0,1) gas01.xml
The example TB nets are in a extended version of pnml standard. To view and edit these nets you can use a custom version of PIPE2 (pipe.zip).
The TB nets presented above are listed based on the dimension of generated state space, from the smallest to the largest. The analysis of the Producer/Consumer example takes less then one second to end and it creates a graph of 6 nodes. The analysis of the Gas Burner (0,1) example, instead, takes more than 7 hours on a Intel Core 2 Duo 1,6 Ghz processor and it builds a graph of 14563 nodes.
To run a state space analysis with Graphgen, put one of the given example in the same folder of graphgen tool and type:
It generates as outputs the graph in binary format (used by the property verification module) and in an annotated DOT text format (used by the GraphViz tool).
To get a graphical view of the state space type:
After you got a .graph file, you can run the tool in verification mode by typing:
It is possible to verify P-invariants from a specified marking. In case of finite graph, it is possible to answer questions about maximum (minimum) of tokens in some (combinations) of places.
The complete list of graphgen options are as follow:
> java -jar graphgen.jar -h
> java -jar graphgen.jar gas05.xml
> dot -Tpdf gas05.dot > gas05.pdf
> java -jar graphgen.jar -c gas05.graph
more info: matteo.camilli@unimi.it
-h
-R
-A
-t<limit>
-c
-o<out.graph>
Print the graphgen synopsis.
Disable relative times.
Disable Time Anonimous replacement.
Set a time limit.
Run graphgen in verification mode.
Set output file.
References
•Bellettini, C.; Capra, L.; , "Reachability Analysis of Time Basic Petri Nets: A Time Coverage Approach," Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2011 13th International Symposium on , vol., no., pp.110-117, 26-29 Sept. 2011 doi: 10.1109/SYNASC 2011.16 URL: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6169509&isnumber=6169489
•Matteo Camilli. 2012. Petri nets state space analysis in the cloud. In Proceedings of the 2012 International Conference on Software Engineering (ICSE 2012). IEEE Press, Piscataway, NJ, USA, 1638-1640.