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

• AlvisEditor
• Getting Started with Alvis Editor

Alvis Compiler is a compiler for Alvis models to its Haskell representation. Current version is in prealpha version and is under huge development. It is a command line program with several options. Standard usage of program was presented in next subsection. Its limitation in current version is discussed in further subsections.

Basic usage of the compiler is to produce an intermediate Haskell representation of an Alvis model. The intermediate representation can be transferred into the dot or Aldebaran format compilation and execution of the Alvis compiler output file - It requires a Haskell compiler to be installed.

$> alvisc input_file.alvis

The default output file is called out.hs. One can include the -o output_file.hs option to specify the name of the output file.

$> alvisc input_file.alvis -o output_file.hs

To compile generated Haskell files, the Alvis.hs module is necessary. The module can be generated the compiler using the -a option:

$> alvisc -a

A short help about the compiler usage can be generated using the -h option:

$> alvisc -h

usage: alvisc file [-a] [--force-generator] [--force-tree-parsing] [-h]
       [-o <file>] [-v]
 -a,--alvis-module         generate Alvis.hs module file instead of
                           compiling any files
    --force-generator      forces compiler to generate output even though
                           compiler met syntactic errors. This option can
                           produce compiler crash.
    --force-tree-parsing   forces semantic analysis even though Alvis parser
                           encountered errors. This option can produce
                           compiler crash.
 -h,--help                 print this message
 -o <file>                 place the output into <file>
 -v,--version              print version information

While parsing, the compiler prints some debug information useful to inform users about errors in compiler and tracking its state (it is the prealpha version) and this output is not switchable-off in the current version.

The compiler stops next parsing levels if an error occurs. To force the generation of the output and/or to force semantic checking one should specify the following options:

$> alvisc --force-tree-parsing --force-generator input_file.alvis -o output_file.hs

These options can cause a compiler crash.

The current compiler version supports only Alvis with α^0 system layer without explicit time specification. The following statements are supported:

• unconditional loop
• conditional loop¹⁾
• if-elseif-else²⁾
• exec³⁾
• pick
• null
• start
• exit
• jump
• in
• out⁴⁾
• select{alt}

Current version do not support:

• commands:
  • ready
  • out constant
• environment specification,
• Alvis with time version,
• Hierarchical agents.

• Added Haskell function specification into source code
• Fixed bug with pick command generation
• Added more debug information of parsing (will be switched off in the future)

• Zip archive download ver: 0.3.2.7
• Tar archive download ver: 0.3.2.7

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.

• Added Alvis LTS to nuXmv translation

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

• Zip archive download ver: 1.0.4
• 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