This is an old revision of the document!
Quick Start
Application launching
The application can be launched by executing PetriNet2ModelChecker.jar file.
Main features
PetriNet2ModelChecker has 3 tab pages:
- Coverability graph to nuXmv parser - facilitates PT-, CP- and RTCP-nets' reachability/coverability graphs to nuXmv code translation.
- Coverability graph to AUT parser - facilitates PT-, CP- and RTCP-nets' reachability/coverability graphs to Aldebaran format translation.
- RTCP Conversion - enables loading RTCP-nets modelled with CPN Tools application and generation of their coverability graphs and simulators.
Steps required to generate nuXmv code for an RTCP-net
- Select the first of the tab pages (Coverability graph to nuXmv parser).
- Select RTCP Nets option from the combo box.
- Enter direct path of the file to translate or select this file using file browser dialog shown after clicking the button designated with […] symbol.
- Click the Translate button
- NuXmv code after its appearance in the memo can be easily saved to a file by clicking on the Save button.
Other functions
Translation of coverability/reachability graphs of other Petri net types to nuXmv code and Aldebaran format can be performed analogously. The process of RTCP nets' coverability graphs and simulators generation is also similar.