Table of Contents
grl2lnt - GRL to LNT translator
grl2lnt [-print pp_file[.grl]]
[-silent | -verbose] [-version] [-about] [-ignore] [-warnings] [-merge] [-sync]
[-warning] [-showall] [-onlyroot] [-force] [-relabel] [-root system] filename[.grl]
GRL (GALS Representation Language) is an imperatively styled
specification language for GALS systems. The grl2lnt program translates
a GRL specification to a LNT specification.
The input to grl2lnt is a GRL
file, which must have the extension .grl. If the user does not specify the
extension .grl on the command line, it will be appended automatically and
grl2lnt will read filename.grl as input.
The principal output of grl2lnt
is a LNT specification named filename.lnt. An auxiliary file can also be
generated if external C code is required, namely filename.fnt, which contains
C code for interfacing external data types and functions.
To avoid clashes
between generated files and user-written files, grl2lnt writes a special
tag at the beginning of each generated file. This tag is a comment containing
the name and the version of grl2lnt that generated the file. grl2lnt uses
this tag to prevent grl2lnt 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, grl2lnt issues an error message and stops.
- -print pp_file[.grl]
- Perform syntax and semantic analysis of filename.grl, prints an indented
form of the file in pp_file.grl and stops execution.
- -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.
- -about
- Display information
about the tool.
- -ignore
- Do not stop execution after an error is issued,
force the generation of an LNT file (possibly with errors).
- -warnings
- Stop
execution when a warning is issued and exit with status 1.
- -merge
- Use merge
mode. It simulates the merge of transitions with adding a special merged
transition and hiding everything else.
- -sync
- Use synchronous mode. It enables
the generation of merged transitions. The option should be used only on
synchronous programs.
- -warning
- No warning is issued.
- -showall
- Show all transitions.
- -onlyroot
- Translate only root system.
- -force
- Overwrite the output files,
even if they were edited by the user or do not need to be updated.
- -relabel
- Generate a rename file to match formal definition of LTS labels (required
by other tools).
- -root instantiation
- where instantiation can take two different
forms: system, or a character string of the form "system (X1, ..., Xn)"
where X1, ..., Xn are values of the constant parameters of the system. It
is highly recommended to type given parameters using syntax of type.
If the option is specified, only the system system will be treated. grl2lnt
will generate a Main process calling the process of the root system in
the LNT specification. By default, if the -root option is absent, it is assumed
that there is only one system in the program or that there exists a system
called Main.
- filename.grl
- GRL specification (input)
- pp_file.grl
- GRL
code (optional output)
- filename.lnt
- LNT code (output)
- filename.fnt
- C code
(optional output)
- filename.ren
- rename file (optional output)
- $GRL_LOCATION
- Needed. The path of directory where GRL is installed.
- $GRL_LOCATION/lnt/GRL_V1.lnt
- GRL predefined library (LNT code)
- $GRL_LOCATION/incl/GRL_V1.h
- GRL predefined library (C code)
If the translation was successful
the exit status is 0. If any error occurred during translation, the exit
status is 1 and error messages are issued.
Eric Leo.
grl
, grl.open
, lnt.open
, lnt2lotos
, caesar.adt
,
caesar
.
Additional information is available from the CADP Web page
located at http://cadp.inria.fr
Directives for installation are given in
files $GRL_LOCATION/INSTALLATION.
Recent changes and improvements to this
software are reported and commented in file $GRL_LOCATION/VERSION.
Some
incorrect GRL programs may be accepted by grl2lnt and translated into
LNT. However, errors will be detected by the LNT and LOTOS compilers lnt2lotos,
caesar and caesar.adt. Please report any bug to cadp@inria.fr
Table of Contents