Table of Contents
traian - compilation of LNT specifications
traian [
-analysis]
[
-c] [
-depend] [
-lotos] [
-noindent] [
-pidlist] [
-main instantiation] [
-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 analysis (i.e., lexical,
syntactic, and semantic checks) and stop before undertaking any code generation.
Mutually exclusive with -c and -lotos. Not a default option.
- -c
- Instruct traian
to perform analysis and, if filename.lnt is a correct LNT program, to generate
C code. Mutually exclusive with -analysis and -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 perform analysis
and, if filename.lnt is a correct LNT program, to prepare information to
be passed to lnt2lotos, which will be invoked afterwards to generate LOTOS
code. Mutually exclusive with -analysis and -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.
- -main instantiation
- where
instantiation is a character string of the form "P
[E1, ..., Em] (V1, ..., Vn)"
that denotes the instantiation of an LNT process. As a special case, instantiation
may also be the keyword "null".
The process P must be defined in the LNT
specification, either directly in filename.lnt or in a transitively included
module. This process should neither have "in out", "out", nor "out var"
parameters.
The list of actual event parameters "[E1, ..., Em]" is optional,
in which case it is assumed to be "[...]". It may also contain named-style parameters
("->") and ellipses ("...").
The list of actual value parameters "(V1, ..., Vn)"
is optional, but only if P has no formal value parameter. It may also contain
named-style parameters provided that each formal value parameter of P is
instantiated (there should be no ellipses). The value parameters V1, ..., Vn
should not contain variables.
This option informs traian that the entry
point of the LNT program is the process call "P [E1, ..., Em] (V1, ..., Vn)",
superseding the MAIN process if it is defined in the LNT program.
If instantiation
is "null", or if the -main option is absent and the LNT program contains
no process, traian, when invoked with its -c option, will generate C code
that does not contain an entry-point "main()" function.
- -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),
lnt2lotos(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
