Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
Both sides next revision
software [2017/01/11 23:04]
marcin
software [2021/09/23 08:51] (current)
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 version and is under huge development. +Current version is in alpha version and is under huge development. To download the Compiler go [[:alvis:start|here]].
-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 //Aldebaran// format compilation +
-and execution of the Alvis compiler output file - It requires a Haskell compiler to be installed. +
-<code> +
-$> alvisc input_file.alvis +
-</code> +
-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. +
-<code> +
-$> alvisc input_file.alvis -o output_file.hs +
-</code> +
-To compile generated Haskell files, the **Alvis.hs** module is necessary. The module can be generated the compiler using the **-a** option: +
-<code> +
-$> alvisc -a +
-</code> +
-A short help about the compiler usage can be generated using the **-h** option: +
-<code> +
-$> alvisc -h +
-</code>+
  
-<code>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</code> 
  
-While parsing, the compiler prints some debug information useful to inform users about +**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: 
-<code> 
-$> alvisc --force-tree-parsing --force-generator input_file.alvis -o output_file.hs 
-</code> 
-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.)) +
-  * **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+  * {{:alvis2modelchecker_v1_1_0.zip|Zip archive download ver: 1.1.0}} 
-  * commands: +  * {{:alvis2modelchecker_v1_1_0-full.zip|Zip archive download ver: 1.1.0 with all Alvis tools included}}
-    * **out** //constant// +
-  * 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 generation +  * Set TRANS section generation as optional in Alvis LTS to nuXmv translation 
-  * Added more debug information of parsing (will be switched off in the future) +===ver: 1.0.6:=== 
-==== Download ==== +  * 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. 
-  * {{:alvisc-0.3.2.52.zip|Zip archive download ver: 0.3.2.52}} +===ver: 1.0.8 (2019-10-05):=== 
-  * {{:alvisc-0.3.2.52.tar|Tar archive download ver: 0.3.2.52}}+  * Labels generation fix 
 +  * State transitions fix 
 +  * Interface fixes  
 +===ver: 1.1.0 (2019-11-24):=== 
 +  * Command line tool added
  
  
Line 108: 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 117: 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}}
   * {{::petrinet2modelchecker_quick_start.pdf|PetriNet2ModelChecker Quick Start}}   * {{::petrinet2modelchecker_quick_start.pdf|PetriNet2ModelChecker Quick Start}}
 +
  
 ====== RTCPNC ====== ====== RTCPNC ======