TRAIAN manual page
Table of Contents

Name

traian - compilation of LNT specifications

Synopsis

traian [-analysis] [-c] [-def F[:T]=V] [-depend] [-lotos] [-noindent] [-pidlist] [-main instantiation] [-silent] [-use filter] [-verbose] [-version] filename[.lnt]

Description

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.

Options

-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.

-def F[:T]=V
Redefine the constant function F so that it returns the value V. Function F must be declared, as a normal or virtual function, in filename.lnt or in a module transitively imported by filename.lnt. This function must not have event parameters nor value parameters. If type T is specified on the command line, the result type of F must be T (the presence of T can be used to resolve overloading ambiguities, if any). There may be several -def options on the command line to redefine distinct functions.

-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.

-use filter
where filter is the absolute pathname to an executable program or shell script that reads as input a list of C function names (one per line) and writes as output a list of 0's or 1's (one per line), the value 1 meaning that the corresponding C function is actually useful and should not be reported as unused by traian.

An example of filter script can be found in file $LNTDIR/src/com/lnt_use. This script is executed by default when the -use option is not given on the command line. The behaviour of this script can be easily adapted by setting the environment variable $LNT_EXTERNAL_FILES.

-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.

Output

If the specification is correct, traian produces a file filename.c that contains the C code generated for the specification.

Diagnostics

When the source is erroneous, error messages are issued. The errors are listed in the filename.err file.

Exit Status

Exit status is 0 if everything is alright, 1 otherwise.

Operands

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)

Environment Variables

$LNTDIR
directory in which TRAIAN is installed (equal to CADP when TRAIAN is used as a component of CADP)

$LNT_EXTERNAL_FILES
list of user files in which C functions should be searched of -silent. to determine if they are useful

Files

$LNTDIR/lib/lnt_predefined.lnt
library of predefined types and functions

$LNTDIR/lib/scheme_*.lnt
libraries of scheme types and functions

$LNTDIR/lib/*.lnt
other libraries (bits, octets, etc.)

$LNTDIR/incl/lnt_predefined.h
C implementation of predefined types and functions

$LNTDIR/bin.`$LNTDIR/com/arch`/lnt_exceptions.o
binary library for exceptions

$LNTDIR/src/com/lnt_use
default filter script

See Also

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

Bugs

Please, send bug reports and remarks to cadp@inria.fr

Authors

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