Table of Contents

Usage of compiler

Basic usage of the compiler is to produce an intermediate Haskell representation of an Alvis model. The intermediate representation may be used to generate the Label Transition System (LTS graph) for the given model. The Alvis compiler 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

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

$> alvisc -h
usage: alvisc file [-ald] [-b <arg>] [-csv] [-dot] [--force-generator]
       [--force-tree-parsing] [-h] [-m <arg>] [-nt] [-o <file>] [-p <arg>]
       [-p1] [-p2] [-sim] [-v] [-vm]
 -ald,--aldebaran          uses code for generating Aldebaran output
 -b,--backend-mode <arg>   switches backend generator. Standard is
                           "default", there is "debug" versionas well.
 -csv,--csv                uses code for generating CSV output
 -dot,--dot                uses code for generating DOT output
    --force-generator      forces compiler to generate output even though
                           compiler met syntactic errors. This option can
                           produce compiler crash.
    --force-tree-parsing   forces sematic analysis even though Alvis
                           parser encountered errors. This option can
                           produce compiler crash.
 -h,--help                 print this message
 -m,--main <arg>           uses code for generating output from given path
 -nt,--no-time             no time
 -o <file>                 place the output into <file>
 -p,--priority <arg>       uses priority algorithm form given path
 -p1,--priority-p1         uses priority algorithm form priority_p1.hs
 -p2,--priority-p2         uses priority algorithm form priority_p1.hs
 -sim,--simulation         uses code for generating simulator
 -v,--version              print version information
 -vm,--verbose-messages    switches on printing additional information
                           about errors which maybe helpful for newbie.

Support of Alvis language and limitation of compiler in current alpha version

The current compiler version supports both time and non-time Alvis models with α^0 system layer (multi-processor systems).

Current version do not support:

Example

Suppose an Alvis model example.alvis is given. The following UNIX/Linux commands generate the LTS graph in the DOT format:

alvisc example.alvis -o example.hs
ghc --make example.hs -o example
./example > example.dot

Compiler options and files

Several compiler options allow to configure the output Haskell program.

The most basic option is for choosing to use time (default) or non-time (–no-time) Alvis version. Resulting programs will use some different data types and algorithms. The second basic option is for choosing to generate standard LTS-printing program (default) or a model simulator (–simulation). Other options allow to select desired format that the resulting program will print (–dot, –csv, –aldebaran or –main path/to/code.hs for an user-defined format) or the priority algorithm to use (–priority-p1, –priority-p2 or –priority path/to/code.hs for an user-defined algorithm).

The standard compiler package comes with compiler-files directory, containing files with Haskell code that the compiler uses, depending on the given options.