====== 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 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.

===== Steps required to generate nuXmv code for an RTCP-net =====
  - Select the first of the tab pages (//Coverability graph to nuXmv parser//). \\ \\ {{:pn2mc:quickstart:tabs.png?400|}}  \\ \\
  - Select //RTCP Nets// option from the combo box.  \\ \\ {{:pn2mc:quickstart:nettypes.png|}}  \\ \\ 
  - Enter direct path of  the file to translate or select this file using file browser dialog shown after clicking the button designated with //[...]// symbol.  \\ \\ {{:pn2mc:quickstart:selectfile.png?400|}}  \\ \\  
  - Click the //Translate// button  \\ \\ {{:pn2mc:quickstart:translate.png|}}  \\ \\
  - NuXmv code after its appearance in the memo can be easily  saved to a file by clicking on the //Save// button.  \\ \\  {{:pn2mc:quickstart:save.png?400|}}  \\ \\


===== 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.




**[[:pn2mc:manual|Go back]]**