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

Go back