Sidebar

Main

Internal

Trace:

Trace: • doc • features • quick_start • compiler • introduction • faq • rtcpn_modelling

Differences

This shows you the differences between two versions of the page.

--- pn2mc:quick_start [2014/11/14 18:31]
jbiernacki created
+++ pn2mc:quick_start [2021/09/23 08:51] (current)
@@ Line 1: / Line 1: @@
 ====== 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]]**