Table of Contents
traian - compilation of LNT specifications
traian [
-analysis]
[
-c] [
-depend] [
-lotos] [
-noindent] [
-pidlist] [
-silent] [
-verbose] [
-version]
filename[
.lnt]
traian is a compiler for LNT. Taking as input
filename.lnt,
which is an LNT program,
traian translates it to C programs and/or a finite
state automaton. This allows to execute, simulate, and/or verify LNT programs.
For the moment, only the syntactic and semantic analyses and the translation
in C of the data part (LNT types and functions) is available.
- -analysis
- Perform lexical, syntactic, and semantic checks and stop before undertaking
code generation. Not a default option.
- -c
- Instruct traian to generate C code.
Opposite of -lotos. Default option.
- -depend
- Display the list of LNT files transitively
included in filename.lnt and stop. If any of these files cannot be opened,
display nothing and stop with exit status 1. Not a default option.
- -lotos
- Instruct traian to generate LOTOS code (not yet implemented). Opposite of
-c. Not a default option.
- -noindent
- Do not format the generated C file filename.c
using indent(1). This can be useful when indent(1) does not exist on the
host machine, or when it crashes with core dumps. Not a default option.
- -pidlist
- List the names of all processes without value parameters that are defined
in the input file filename.lnt. This option is used by the EUCALYPTUS graphical
user interface to propose all processes that can be used as a main process.
- -silent
- Execute silenty. Opposite of -verbose. Not a default option.
- -verbose
- Animate the user's screen, telling what is going on. Opposite of -silent. Default
option.
- -version
- Display the current version number of the software and stop.
Not a default option.
If the specification is correct,
traian produces
a file
filename.c that contains the C code generated for the specification.
When the source is erroneous, error messages are issued. The
errors are listed in the
filename.err file.
Exit status is 0 if
everything is alright, 1 otherwise.
- filename.lnt
- LNT specification
(input)
- filename.t
- external C implementation for types (input)
- filename.f
- external C implementation for functions (input)
- filename.c
- generated C code
(output)
- filename.err
- detailed error messages (output)
- $LNTDIR/lib/lotosnt_predefined.lnt
- declaration of predefined types and functions
- $LNTDIR/incl/lotosnt_predefined.h
- C implementation of predefined types and functions
- $LNTDIR/bin.`$LNTDIR/com/arch`/lotosnt_exceptions.o
- binary library for exceptions
indent(1)
For the concrete syntax
supported by traian refer to the "Compiler documentation" (file doc.ps)
in the `doc' directory of the distribution.
Additional information is available
from the TRAIAN Web page located at http://vasy.inria.fr/traian
Directives
for installation are given in file $LNTDIR/INSTALLATION.txt
Features of
the current release of this software are reported in file $LNTDIR/=README.txt
Recent changes and improvements to this software are reported and commented
in file $LNTDIR/HISTORY.txt
The known problems of the current release are
reported in file $LNTDIR/KNOWN_PROBLEMS.txt
Please, send bug reports
and remarks to
cadp@inria.fr
Versions 2.* of TRAIAN have been written
by Mihaela Sighireanu, Xavier Bouchoux, David Champelovier, Claude Chaudet,
Nicolas Descoubes, Hubert Garavel, Yves Guerte, Marc Herbert, Remi Herilier,
Alain Kaufmann, Frederic Lang, Vincent Powazny, Wendelin Serwe, and Bruno
Vivien.
Versions 3.* of TRAIAN have been written by Hubert Garavel, Frederic
Lang, and Wendelin Serwe.
Table of Contents
