Table of Contents
traian - compilation of LNT specifications
traian [
-analysis]
[
-c] [
-depend] [
-lotos] [
-noindent] [
-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 dependencies
of filename.lnt and stop. 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.
- -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