PetriNet2ModelChecker features overview

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.

This tab page contains features enabling RTCP-nets compilation and generation of their coverability graphs.

It looks similar to the other two tab pages. In its top panel there are 4 different types of RTCP-nets processing operations:

• CPN Tools » RTCP - Translation of RTCP-net modelled in CPN tools to original RTCP xml format which can be later compiled by the RTCPNC (RTCP-net compiler). This translation is possible due to integration with cpn2rtcpn tool.
• RTCP net » RTCP simulator - RTCP-net compilation in RTCPNC compiler. As a result of this operation executable jar with simulator of the model is created. User can select the desired location for the output files.
• RTCP net » Coverability graph - Generation of RTCP-net's coverability graph. This option involves compiling the model in RTCPNC and then executing the generated simulator to obtain coverability graph of the input net.
• CPN Tools » Coverability graph - Direct conversion from CPN Tools file containig RTCP-net to its coverability graph. This step is concatenation of options 1 and 3.

In the bottom panel except from the Save there is a Export to pdf button. Whilst the first one is doing exactly the same thing as in other tab pages, the second one is a feature which enables automatic pdf generation for the coverability graph stored in the memo field. This feature works only if the distribution of Graphviz tool is properly installed on the machine. This feature considerably speeds up the process of model verification because user can immediately see the visual representation of the generated coverability graph.

After a coverability graph of an RTCP-net is generated it can be used as an input to the translation algorithms and be verified in nuXmv and CADP model checkers.

Top menu bar contains 4 submenus:

• File - containing Open and Exit buttons. First one of them allows to select a file from a file system - its path appears in the current tab page's select file edit. The other is obvious.
  
  
• Parser - contains translation settings. Currently there is only one parameter that can be set. It is called omega and represents the number of tokens which will be treated as infinity during PT-nets coverability graphs translation.
  
  
  
• RTCP Simulator - contains options of RTCP-nets compilation and coverability graph generation. Currently there is only one parameter that can be set - RTCP simulation End time. It sets maximal virtual time of simulation during coverability graph generation. If this time is reached, coverabilty graph generation will stop.
  
  
  
  
• Help - Contains some basic information about the application.

Go back