Alvis Editor is an editor for Alvis models. It supports both the design of hierarchical communication diagrams and the implementation of the code layer. To download the Editor go here.

Alvis Compiler is a compiler for Alvis models to its Haskell representation. Current version is in alpha version and is under huge development. To download the Compiler go here.

Alvis2ModelChecker tool deals with the problem of translation of Alvis LTS into SMV language suppoerted by nuXmv / NuSMV tools.

• Zip archive download ver: 1.1.0
• Zip archive download ver: 1.1.0 with all Alvis tools included

• Added Timed Alvis LTS to nuXmv translation
• Set TRANS section generation as optional in Alvis LTS to nuXmv translation

• Added Petri&Alvis2ModelChecker application that contains an option to simplify Alvis LTS to nuXmv translation, by storing only model's Parameters Values in the nuXmv variables.

• Labels generation fix
• State transitions fix
• Interface fixes

• Command line tool added

PetriNet2ModelChecker tool deals with the problem of translation of reachability graphs for place-transition, coloured and real-time coloured Petri nets into the NuXMV language and Aldebaran format. PetriNet2ModelChecker works with reachability graphs generated respectively by the TINA, CPN Tools and RTCPNC software. Thus, it provides the possibility of formal verification of Petri nets designed with these environments using model checking techniques and mainstream model checkers - nuXmv for LTL and CTL temporal logics, CADP Evaluator for regular alternation-free mu-calculus. It also integrates cpn2rtcpn and rtcpnc software and allows to load RTCP nets modelled in CPN Tools and generate their coverability graphs or simulators.

PetriNet2ModelChecker manual can be found here: Online PetriNet2ModelChecker Manual.

• Updated algorithm of translation of RTCP-nets coverability graphs to nuXmv langage.
• Fixed minor bugs regarding GUI
• New version of RTCP-net compiler (4.2) - optimization + graph generation fixes.

• Fixed file loading bug
• Minor updates in the algorithm of translation of RTCP-nets coverability graphs to nuXmv langage.

• Interface fixes

• Zip archive download ver: 1.0.7
• PetriNet2ModelChecker Quick Start

RTCPNC (Real-Time Coloured Petri Net Compiler) is a compiler for RTCP-nets. It is a simple command line application. Standard usage of the program is presented in next subsection. RTCPNC is integreted into PetriNet2ModelChecker tool which facilitates usage of the compiler by providing intuitive graphical user interface.

The application runs on the Java virtual machine in command-line environment. To run the application one has to type the command:

$> java -jar rtcpnc.jar {RTCP-net model} {simulator name}

where:

• RTCP-net model – XML file with RTCP-net model.
• simulator name – Any simulator name

Execution of this command starts the process of simulator generation. Every important event during the compilation is reported in the console window. It enables quick error tracking if any occurs in the model. Due to the fact that even the smallest model can generate more then 1000 lines of diagnostic information, it is recommended to use output redirection to the chosen log file:

$> java -jar rtcpnc.jar {RTCP-net model} {simulator name} > {log file name}

Simulator generated by the compiler is in the directory with the name specified in a {simulator name} parameter of rtcpnc.jar. The simulator directory contains the following subdirectories and files:

• src - The source directory, this directory contains all the source code files generated by RTCPNC. One can edit these files according to ones needs.
• lib - directory of modules required to run the simulator.
• class - a catalog compiled class files created by compiling the src directory.
• META-INF - directory containing the manifest file, needed to build the correct executable file.
• {simulator name}.jar - simulator executable file.

The above-mentioned list of files and directories is a complete set generated by the application. However, for the proper functioning of the simulator, {simulator name}.jar file and lib directory is sufficent.

Simulator, similarly to the generator, runs on the Java virtual machine console environment. To run the simulator, the following command is used:

$> java -jar {simulator name}.jar {simulation time}

where:

• simulator name - the name of the generated simulator
• simulation time - an integer specifying how many simulation steps are to be executed

To generate reachability or coverability graph instead of running the simulation, -rg and -cg options can be used:

$> java -jar {simulator name}.jar {simulation time} -cg

$> java -jar {simulator name}.jar {simulation time} -rg

• Zip archive download ver: 4.2