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/02/19 09:25] 127.0.0.1 external edit | 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 12: | 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.52.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 111: | 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 120: | 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 ====== | ||