TRAIAN manual page
Table of Contents

Name

traian - compilation of LNT specifications

Synopsis

traian [-analysis] [-c] [-depend] [-lotos] [-noindent] [-silent] [-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 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.

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

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)

Files

$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

See Also

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

Bugs

Please, send bug reports and remarks to [email protected]

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