This is an old revision of the document!


PetriNet2ModelChecker features overview

Main features

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.


Coverability graph to nuXmv parser


Coverability graph to AUT parser


RTCP Conversion