Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionBoth sides next revision | ||
software [2016/01/20 20:50] ptm [Alvis Editor] | software [2021/09/23 08:51] (current) | ||
---|---|---|---|
Line 3: | Line 3: | ||
====== Alvis Editor ====== | ====== Alvis Editor ====== | ||
- | **Alvis Editor** is an editor for Alvis models. It supports both the design of hierarchical communication diagrams and the implementation of the code layer. | + | **Alvis Editor** is an editor for Alvis models. It supports both the design of hierarchical communication diagrams and the implementation of the code layer. |
- | * [[: | ||
Line 11: | Line 11: | ||
**Alvis Compiler** is a compiler for Alvis models to its Haskell representation. | **Alvis Compiler** is a compiler for Alvis models to its Haskell representation. | ||
- | Current version is in prealpha | + | Current version is in alpha 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. | + | |
- | ==== Usage of compiler ==== | ||
- | Basic usage of the compiler is to produce an intermediate Haskell representation of an Alvis model. | + | ====== Alvis2ModelChecker ====== |
- | The intermediate representation can be transferred into the //dot// or // | + | |
- | 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 | + | |
- | </ | + | |
- | < | ||
- | [-o < | ||
- | | ||
- | | ||
- | --force-generator | ||
- | | ||
- | | ||
- | --force-tree-parsing | ||
- | | ||
- | | ||
- | | ||
- | -o < | ||
- | | ||
- | While parsing, | + | **Alvis2ModelChecker** tool deals with the problem of translation of Alvis LTS into SMV language suppoerted by nuXmv / NuSMV tools. |
- | 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. | ||
- | + | ==== Download | |
- | ==== Support of Alvis language and limitation of compiler in current alpha version | + | |
- | The current compiler version supports only Alvis with α^0 system layer without explicit time specification. | + | * {{: |
- | The following statements are supported: | + | * {{: |
- | * unconditional **loop** | + | |
- | * conditional **loop**((The usage of Haskell functions within a condition is limited to Prelude library only. The full Haskell syntax is not supported yet.)) | + | |
- | * **if**-**elseif**-**else**((The usage of Haskell functions within a condition is limited to Prelude library only. The full Haskell syntax is not supported yet.)) | + | |
- | * **exec**((The usage of Haskell functions is limited to Prelude library only. The full Haskell syntax is not supported yet.)) | + | |
- | * **pick** | + | |
- | * **null** | + | |
- | * **start** | + | |
- | * **exit** | + | |
- | * **jump** | + | |
- | * **in** | + | |
- | * **out**((Only parameters (variables) can be used as the second argument.)) | + | |
- | * **select{alt}** | + | |
- | + | ||
- | Current version __do not__ support: | + | |
- | * commands: | + | |
- | * **ready** | + | |
- | * **out** // | + | |
- | * environment specification, | + | |
- | * Alvis with time version, | + | |
- | * Hierarchical agents. | + | |
==== Changelog ==== | ==== Changelog ==== | ||
- | + | ===ver: 1.0.5:=== | |
- | * Added Haskell function specification into source code | + | * Added Timed Alvis LTS to nuXmv translation |
- | * Fixed bug with pick command | + | * Set TRANS section |
- | * Added more debug information of parsing (will be switched off in the future) | + | ===ver: 1.0.6:=== |
- | ==== Download ==== | + | * Added Petri& |
- | * {{:alvisc-0.3.2.7.zip|Zip archive download | + | ===ver: 1.0.8 (2019-10-05): |
- | * {{: | + | * Labels generation fix |
+ | * State transitions fix | ||
+ | * Interface fixes | ||
+ | ===ver: 1.1.0 (2019-11-24): | ||
+ | * Command line tool added | ||
Line 110: | Line 52: | ||
==== Changelog ==== | ==== Changelog ==== | ||
- | ===ver: 1.0.2:=== | ||
- | * Added Alvis LTS to nuXmv translation | ||
===ver: 1.0.3:=== | ===ver: 1.0.3:=== | ||
* Updated algorithm of translation of RTCP-nets coverability graphs to nuXmv langage. | * Updated algorithm of translation of RTCP-nets coverability graphs to nuXmv langage. | ||
Line 119: | Line 59: | ||
* Fixed file loading bug | * Fixed file loading bug | ||
* Minor updates in the algorithm of translation of RTCP-nets coverability graphs to nuXmv langage. | * Minor updates in the algorithm of translation of RTCP-nets coverability graphs to nuXmv langage. | ||
+ | ===ver: 1.0.7:=== | ||
+ | * Interface fixes | ||
+ | |||
==== Download ==== | ==== Download ==== | ||
- | * {{:petrinet2modelchecker_v1_0_4.zip|Zip archive download ver: 1.0.4}} | + | * {{:petrinet2modelchecker_v1_07.zip|Zip archive download ver: 1.0.7}} |
* {{:: | * {{:: | ||
+ | |||
====== RTCPNC ====== | ====== RTCPNC ====== |