PetriKit Manual

Conrado P.L.G. (conradoplg at gmail.com), 2008-01-17

PetriKit is composed of a tool set. In order to analyze of Petri Nets, you must use them together.

Setup

Windows version

Sorry, there is no installer at the moment. Just extract the zip file and add the PetriKit folder to your PATH environment variable.

Linux/others version

You must have Python 2.5 or greater installed in your system.

Download the distribution package and uncompress it. A "PetriKit-1.0" (or similar) folder will be created. Open a console in it as a root/administrator and execute the following command:

python2.5 setup.py install

(Change python2.5 to whichever version you have, if you have a more recent version)

The tools will be installed in the Scripts folder inside the Python distribution. In order to execute the tools only by their names, add that folder to the PATH environment variable.

You must now install some libraries on which PetriKit depends. They are: NumPy, SimpleParse and Cheetah. All of them have the same setup procedures.

Quick Guide

To generate the acessibility graph of a Petri Net

Say you have a net in the net.xml file, with the PNML format. Use:

petrikit-compile-net.py net.xml | petrikit-enumerate-states.py | petrikit-format-graph.py -o graph.html

The acessibility graph will be written in graph.html. You may specify a file with .txt, .xml or .dot extension in order to generate a report in those formats. The .dot format can be used by the GraphViz software to generate a image representation of the graph.

To extract the basic properties of a Petri Net

Say you have a net in the net.xml file, with the PNML format. Use:

petrikit-compile-net.py net.xml | petrikit-enumerate-states.py | petrikit-properties.py -o properties.html

The basic properties report will be written in properties.html. You may specify a file with .txt or .xml extension in order to generate a report in those formats.

To extract the invariants of a Petri Net

Say you have a net in the net.xml file, with the PNML format. Use:

petrikit-compile-net.py rede.xml | petrikit-invariants.py -o invariants.html

The invariants report will be written in invariants.html. You may specify a file with .txt or .xml extension in order to generate a report in those formats.

Tool specific documentation

petrikit-compile-net

The compiler tool reads a Petri Net file, parses it and writes the output in a internal format of PetriKit. You may save the output to a file if you are going to do several analysis of the net in order to avoid parsing the net multiple times. But most of the time the parsing time is negligible, so you may redirect the output of the compiler directly to other tool.

The -f switch specifies the format of the input net; it can be omitted, in that case the tool will guess the format based on the extension of the file.

The -o switch specifies an output file; if omitted, or if the file specified is "-", then the output will be written to the standard output.

The argument passed is the input file. If it is omitted, or if it is "-", then the standard input will be read.

The input formats currently supported are the PNML format (extension: xml or pnml) and the RDP format (extension: rdp) of the ARP tool.

petrikit-format-net

The net formatter tool reads a compiled Petri Net file generated by the compiler tool and writes it in a specified format. You may use this tool with the compiler tool in order to convert nets between differente formats. For example, you can convert from PNML to RDP with:

petrikit-compile-net.py net.xml | petrikit-format-net.py -o net.rdp

The -f switch specifies the format of the output net; it can be omitted, in that case the tool will guess the format based on the extension of the output file.

The -o switch specifies an output file; if omitted, or if the file specified is "-", then the output will be written to the standard output.

The argument passed is the input file. If it is omitted, or if it is "-", then the standard input will be read.

The output formats currently supported are the PNML format (extension: xml or pnml) and the RDP format (extension: rdp) of the ARP tool.

petrikit-enumerate-states

The enumerator tool reads a compiled Petri Net file, generates its reachability graph and writes it in a internal format to the output.

The -o switch specifies an output file; if omitted, or if the file specified is "-", then the output will be written to the standard output.

The argument passed is the input file. If it is omitted, or if it is "-", then the standard input will be read.

petrikit-format-graph

The graph formatter tool reads a compiled reachability graph file generated by the enumerator tool and writes it in a specified format.

The -f switch specifies the format of the output graph; it can be omitted, in that case the tool will guess the format based on the extension of the output file.

The -o switch specifies an output file; if omitted, or if the file specified is "-", then the output will be written to the standard output.

The argument passed is the input file. If it is omitted, or if it is "-", then the standard input will be read.

The output formats currently supported are the TXT, HTML, XML, and DOT formats. The TXT and HTML are suited to human reading, and the XML to storage and further processing. The DOT file can be used by the GraphViz tool to generate an image of the graph.

petrikit-properties

The basic properties extractor tool reads a compiled reachability graph file generated by the enumerator tool, extracts the basic properties using it and writes a report to the output file.

The -f switch specifies the format of the output report; it can be omitted, in that case the tool will guess the format based on the extension of the output file.

The -o switch specifies an output file; if omitted, or if the file specified is "-", then the output will be written to the standard output.

The argument passed is the input file. If it is omitted, or if it is "-", then the standard input will be read.

The output formats currently supported are the TXT, HTML and XML formats. The TXT and HTML are suited to human reading, and the XML to storage and further processing.

petrikit-invariants

The basic properties extractor tool reads a compiled Petri Net file, extracts the invariants and writes a report to the output file.

The -f switch specifies the format of the output report; it can be omitted, in that case the tool will guess the format based on the extension of the output file.

The -o switch specifies an output file; if omitted, or if the file specified is "-", then the output will be written to the standard output.

The argument passed is the input file. If it is omitted, or if it is "-", then the standard input will be read.

The output formats currently supported are the TXT, HTML and XML formats. The TXT and HTML are suited to human reading, and the XML to storage and further processing.