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.
The current compiler version supports both time and non-time Alvis models with α^0 system layer (multi-processor systems).
Current version do not support:
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
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.