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.

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 contains the most important functionalities: input file selection, Petri Net type selection and Translate button.

In the input file text field should contain the valid path of the file containing the reachability/coverabilty graph of a Petri Net type selected in Petri Net type selection combo box. Currently there are 3 different types of Petri Nets available for translation - place transition Petri nets, coloured Petri Nets and Real-time coloured Petri nets. Each one of these Petri net types needs a different format of an input file:

• .kts - for coverability graphs of PT-nets (export instructions for TINA tool).
• .cpn - for reachability graphs of CP-nets (generation instructions for CPN Tools).
• .dot - for coverability graphs of RTCP-nets (RTCP compiler usage).

Translate button is responsible for the initiation of the actual translation process.

Memo field will contain the generated nuXmv code after the successful completion of graph translation. It's content can be edited once the translation is done. Thus, there is a possibility to i.e. add some LTL or CTL formulae before saving the nuXmv code to the file.

Bottom panel contains only one button. Save is responsible for storing the content of the memo in the selected location.

This tab page contains features connected to Aldebaran file generation.

It looks exactly the same as the Coverability graph to nuXmv parser tab page. It also has the same functionalities. The only difference is that in Memo field aldebaran graph code will appear instead of nuXmv code.

Go back