LNT.OPEN manual page


What is CADP?
Home Page Tools Overview Current Status Recent Changes
Installation
How to obtain CADP? Usage Statistics
Documentation
FAQ Tutorials Publications Manual Pages Demo Examples Wikipedia
CADP Community
Newsletters Education & Training Case Studies Research Tools
CADP Resources
VLPN Benchmarks VLSAT Benchmarks VLTS Benchmarks Other Resources
About CADP
Contributors

Name

lnt.open - OPEN/CAESAR connection for the LNT language

lnt.open [-def F[:T]=V] [-depend] [-force] [-main root-process] [-silent | -verbose] [-version] [lotos_options] filename[.lnt] [cc_options] prog[.a|.c|.o] [prog_options]

Description

Taking as input filename.lnt (which contains the principal module of a LNT specification) and an OPEN/CAESAR program prog[.a|.c|.o], lnt.open operates as follows:

First, it invokes traian on filename.lnt to perform static and semantic analyses on this file and all its transitively imported modules, and stops in case of errors.

Second, it translates filename.lnt (and all its transitively imported modules) into a LOTOS specification using lnt2lotos .

Third, it calls ``lotos.open filename.lotos [cc_options] prog[.a|.c|.o] [prog_options]'', passing to lotos.open , and, transitively, to caesar.adt and caesar , appropriate options that depend on the options passed to lnt.open (see below).

However, if prog is the "-" string (instead of the name of an OPEN/CAESAR application program), lnt.open will execute only the first two steps (analysis and translation into a LOTOS specification) and then stop without invoking lotos.open . In such case, the files generated during the first two steps are not removed, thus allowing the generated LOTOS specification to be used for other purposes than OPEN/CAESAR (e.g., for rapid prototyping with EXEC/CAESAR).

Options

-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: List all the LNT files transitively included in filename.lnt and exit. Not a default option.
-force: Overwrite output files, even if they were edited by the user or do not need to be updated. This option is passed to lnt2lotos and lotos.open .
-main process-instantiation: Use the process process-instantiation as the main process. It is an error if the LNT specification does not contain a corresponding process definition. This option is passed to lnt2lotos .
-silent: Execute silently. This option is passed to lnt2lotos and lotos.open .
-verbose: Report in detail activities and progress, including errors and messages emitted by auxiliary tools, to the user's screen. This option is passed to lnt2lotos and lotos.open .
-version: Display the version number of lnt2lotos and stop.
lotos_options: if any, are passed to lotos.open .
cc_options: if any, are passed to the C compiler.
prog_options: if any, are passed to prog.

Operands

filename.lnt: LNT specification (input)
filename.tnt: C code for data types (source, input)
filename.fnt: C code for functions (source, input)
filename.o: object code (output)
filename.err: detailed error messages (output)
prog.a: exploration module (archive, input)
prog.c: exploration module (source, input)
prog.o: exploration module (object code, input)
prog: executable program (output)

Files

$CADP_TMP/lnt.*: temporary files
$CADP/lib/LNT_V1.lib: LNT predefined library (LOTOS code)
$CADP/incl/LNT_V1.h: LNT predefined library (C code)

Name
Synopsis
Description
Options
Operands
Files
Exit Status
Authors
See Also
Bugs