LNT2LOTOS manual page
Table of Contents

Name

lnt2lotos - LOTOS NT to LOTOS translator

Synopsis

lnt2lotos [-silent | -verbose] [-version] [-force] [-pidlist] [-root instantiation] filename[.lnt]

Description

LOTOS NT is an imperatively styled specification language for concurrent processes. The lnt2lotos program translates a LOTOS NT specification to a LOTOS specification.

The input to lnt2lotos is a LOTOS NT file, which must have the extension .lnt. If the user does not specify the extension .lnt on the command line, it will be appended automatically and lnt2lotos will read filename.lnt as input. External C code can be provided by auxiliary files, namely filename.tnt for data type definitions and filename.fnt for function definitions.

Typically, the input should have been pre-processed by lpp before being passed to lnt2lotos. The pre-processor expands extended notation such as literal numbers and strings, which is not accepted by lnt2lotos directly.

The output is a LOTOS library or LOTOS specification. When lnt2lotos is called with the -root option and the name of an instantiation, or when the input specification contains a process called MAIN without value parameters, lnt2lotos will generate a LOTOS specification. In all other cases, lnt2lotos will generate a LOTOS library. Two auxiliary files are also generated, namely filename.t, which contains C code for external data types, and filename.f, which contains C code for external functions. Note that filename.t includes filename.tnt (if present), and that filename.f includes filename.fnt (if present).

To avoid confusion between source code and generated code, all output files created by lnt2lotos will be placed in a special directory that lnt2lotos creates if it does not exist already. If the creation of the direcory fails, lnt2lotos issues an error message and stops. The name of this directory is either given by the environment variable $LNTGEN, if this variable is set, or is ./LNTGEN. Note that ./LNTGEN (or $LNTGEN) is created relative to the directory from which the user calls lnt2lotos, not relative to the directory containing the input file.

The name of the input file is used to construct the names of the output files, with the particular rule that all letters are turned to upper case when constructing the names of .lib files. For an input file example.lnt, lnt2lotos creates the LOTOS library EXAMPLE.lib or the LOTOS specification example.lotos, and two auxiliary files example.t and example.f. To avoid clashes between generated files and user-written files, lnt2lotos writes a special tag at the beginning of each generated file. This tag is a comment containing the name and the version of lnt2lotos that generated the file. lnt2lotos uses this tag for two purposes:

Options

-silent
Execute silently, reporting only errors. This is the opposite of -verbose. The default option is -verbose.

-verbose
Report activities and progress, including errors, to the user's screen. This is the opposite of -silent. The default option is -verbose.

-version
Display the tool version and exit.

-force
Overwrite the output files, even if they were edited by the user or do not need to be updated.

-pidlist
List the names of all processes without value parameters that occur in the input file and exit. In other words, list all processes that can be used as main process (by instantiation with the -root option).

-root instantiation
Use the process instantiation as the main process, meaning that the generated LOTOS specification has the behaviour of the main process. The instantiation is a character string (preferably enclosed by single quotes) denoting a LOTOS NT process instantiation. For example, given the instantiation P [G1, ..., Gn] of process P with gate identifiers [G1, ..., Gn] lnt2lotos would produce a specification specification P [G1, ..., Gn] : exit with a behaviour behaviour P [G1, ..., Gn] where .... If the list of gates [G1, ..., Gn] is omitted, the list of formal gate parameters of the process P is used instead. The process P, of which there can be exactly one (processes cannot be overloaded in LOTOS NT), should have no value parameters at all. If the option ``-root -'' is specified (that is, the instantiation is specified as ``-''), this indicates that there is no main process (even if there is a process called MAIN), and lnt2lotos will generate a LOTOS library.

Operands

filename.lnt
LOTOS NT specification (input)

filename.tnt
C code for data types (input)

filename.fnt
C code for functions (input)

$LNTGEN/*.sig
imported modules signatures (input)

$LNTGEN/filename.lotos
LOTOS code (optional output)

$LNTGEN/FILENAME.lib
LOTOS code (optional output)

$LNTGEN/filename.t
C code (output)

$LNTGEN/filename.f
C code (output)

$LNTGEN/filename.err
detailed error messages (output)

$LNTGEN/filename.sig
module signature (output)

Files

$CADP/lib/LNT_V1.lib
LOTOS NT predefined library (LOTOS code)

$CADP/incl/LNT_V1.h
LOTOS NT predefined library (C code)

Environment Variables

$LNTGEN
The target directory of the output files.

Exit Status

If the translation was successful the exit status is 0, even if warnings were issued during the execution. If any error occurred during translation, the exit status is 1.

Authors

David Champelovier, Xavier Clerc, Hubert Garavel, Gideon Smeding, Frederic Lang, Wendelin Serwe (INRIA Rhone-Alpes)

See Also

For a complete description of LOTOS NT, see the lnt2lotos reference manual. Otherwise see lpp , lnt.open , caesar.adt , caesar .

Bugs

The type system of lnt2lotos is not implemented yet, hence, some incorrect LOTOS NT programs will be accepted by lnt2lotos. These errors will be detected by the LOTOS compilers caesar and caesar.adt. Please report any mistranslations or other problems with lnt2lotos to cadp@inria.fr

Table of Contents