This is an old revision of the document!
PetriNet2ModelChecker features overview
Main features
PetriNet2ModelChecker has 3 tab pages which contain three different groups of features:
- Coverability graph to nuXmv parser - facilitates PT-, CP- and RTCP-nets' reachability/coverability graphs into nuXmv code translation.
- Coverability graph to AUT parser - facilitates PT-, CP- and RTCP-nets' reachability/coverability graphs into Aldebaran format translation.
- RTCP Conversion - enables loading RTCP-nets modelled with CPN Tools application and generation of their coverability graphs and simulators.
Each one of these tab pages is presented below.
Coverability graph to nuXmv parser
This tab page contains features connected to nuXmv code generation.
The tab page consists of 3 main areas: top panel, memo field and bottom panel.
Top panel
Top panel contains the most important functionalities: input file selection, Petri Net type selection and Translate button.