This is an old revision of the document!
Alvis Editor
Changelog
ver: 1.0.2:
- Added Alvis LTS to nuXmv translation
ver: 1.0.3:
- 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.
ver: 1.0.4:
- Fixed file loading bug
- Minor updates in the algorithm of translation of RTCP-nets coverability graphs to nuXmv langage.
Download
RTCPNC
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.
Compiler usage
Compiler
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
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