Table of Contents
lnt2lotos - LNT to LOTOS translator
] [-more command
] [-root instantiation
LNT (LOTOS New Technology, formerly noted LOTOS NT) is an imperatively
styled specification language for concurrent processes. The lnt2lotos
translates a LNT specification to a LOTOS specification.
The input to lnt2lotos
is a LNT file, whose name should contain only letters, digits, and underscores,
and which must have the extension
.lnt. If the user does not specify the
.lnt on the command line, this extension will be appended automatically,
so that lnt2lotos will read filename
.lnt as input. External C code can be
provided by auxiliary files, namely filename
.tnt for data type definitions
.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 principal output of lnt2lotos is
a LOTOS specification named filename
.lotos (unless the -root null option
is used, in which case a LOTOS library FILENAME
.lib is generated instead;
see below for further details). Two auxiliary files are also generated,
.t, which contains C code for external data types, and filename
which contains C code for external functions. Note that 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 directory 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 by default. Note that
$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.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:
- To prevent
lnt2lotos from overwriting a file that was not generated by itself: if
the output file already exists but has no special tag or has an invalid
tag indicating that the file was not generated by the right tool, lnt2lotos
issues an error message and stops.
- To avoid unnecessary compilations: lnt2lotos
recompiles a LNT file only if the source file was modified since the last
translation, or if the output file was generated by an older version of
- Execute silently, reporting only errors. This is
the opposite of -verbose. The default option is -verbose.
- Report activities
and progress, including errors, to the user's screen. This is the opposite
of -silent. The default option is -verbose.
- Display the tool version
- Overwrite the output files, even if they were edited by
the user or do not need to be updated.
- -more command
- Use command to display
the error messages, instead of "$CADP/src/com/cadp_more", which is the
default. command is a shell command (preferably enclosed in quotes or double
quotes) containing the pathname of the chosen pager, possibly followed
by a list of options. Not a default option.
- 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 a main process having
no value parameter (by instantiation with the -root option). This option
is used by the EUCALYPTUS graphical user interface.
- -root instantiation
instantiation can take three different forms: module, null, or a character
string of the form "P [G1, ..., Gm] (V1, ..., Vn)" according to the syntax for
a process instantiation given in the reference manual [Champelovier-Clerc-Garavel-et-al-10].
By default, if the "-root" option is absent, it is assumed to be of the
third form and identical to "-root
If the option "-root module" is specified, lnt2lotos will generate a LOTOS
library (i.e., a "
.lib" file without main behaviour). If the LNT specification
contains a process called MAIN, it will be treated like an ordinary process.
If the option "-root null" is specified, lnt2lotos will generate a LOTOS
specification whose main behaviour is "stop". If the LNT specification contains
a process called MAIN, it will be treated like an ordinary process.
In the third case, lnt2lotos will generate a LOTOS specification whose
main behaviour is the instantiation of process P with actual gate identifiers
[G1, ..., Gm] and actual value parameters (V1, ..., Vn).
As processes cannot be overloaded in LNT, there must be at most one process
called P in the LNT specification, either directly defined in filename
or defined in a included module included transitively.
The list of actual gate parameters is optional; if this list is missing
and if filename
.lnt does not contain a process named P, an empty list of
gate parameters is assumed; if this list is missing and if filename
contains a process named P, lnt2lotos will replace a missing list of actual
gate parameters by the list of formal gate parameters of the process P.
If process P is defined in filename
.lnt, the list of actual gate parameters
can also be given using named-style parameters (``
=>'') and ellipses (``
The list of actual value parameters is also optional; if this list is missing,
an empty list of value parameters is assumed. It should only contain algebraically-closed
terms (i.e., contain no variables) and be compatible, in number and types,
with the list of formal variable parameters of process P. Process P should
have only in parameters (i.e., no out or inout parameter). If the actual value
parameters use rich-term syntax notations [Champelovier-Clerc-Garavel-et-al-10,
chapter 3], these notations must be expanded before invoking lnt2lotos;
this is automatically performed by lnt.open
which calls lpp
to expand rich-term syntax before invoking lnt2lotos.
- LNT specification (input)
- C code for data types (input)
- C code for functions (input)
- imported modules signatures (input)
- LOTOS code (optional output)
- LOTOS code (optional output)
- C code (output)
- C code (output)
- detailed error messages (output)
- module signature (output)
- LNT predefined library
- LNT predefined library (C code)
- The target directory of the output files.
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.
David Champelovier, Xavier Clerc, Hubert Garavel,
Gideon Smeding, Frederic Lang, Wendelin Serwe (INRIA Rhone-Alpes)
, and the "Reference
Manual of the LNT to LOTOS Translator" available from http://cadp.inria.fr/publications/Champelovier-Clerc-Garavel-et-al-10.html
Additional information is available from the CADP Web page located at http://cadp.inria.fr
Directives for installation are given in files $CADP/INSTALLATION_*.
changes and improvements to this software are reported and commented in
The type system of lnt2lotos
is not implemented
in full detail, hence, some incorrect LNT programs will be accepted by
and translated into LOTOS. However, these errors will be detected
by the LOTOS compilers caesar
. Please report any mistranslations
or other problems with lnt2lotos
Table of Contents