Table of Contents
grl.open - OPEN/CAESAR connection for the GRL language
grl.open
[-print pp_file[.grl]] [-silent | -verbose] [-version] [-about] [-ignore] [-warnings]
[-merge] [-sync] [-warning] [-showall] [-force] [-relabel] [-root system] [-labels]
[lnt_options] filename[.grl] [cc_options] user[.a|.c|.o] [user_options]
Taking
as input filename.grl (which contains the principal program of a GRL specification)
and an OPEN/CAESAR program user[.a|.c|.o], grl.open operates as follows:
- First,
it translates the GRL specification filename.grl (including all transitively
imported programs) into a LNT specification using grl2lnt
. See grl2lnt
for more information.
- Then, it calls ``lnt.open [lnt_options] filename.lnt
[cc_options] user[.a|.c|.o] [user_options]'', passing to lnt.open (and, transitively,
caesar.open, caesar.adt and caesar) appropriate options that depend on the
options passed to grl.open (see below). See lnt.open
, caesar.open
,
caesar.adt
, and caesar
for more information.
However, if user is the "-" string (instead of the name of an OPEN/CAESAR
application program), grl.open will execute only the first step (translation
into a LNT specification) and then stop without invoking lnt.open. In such
case, the files generated during the first step are not removed.
- -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. This option is passed to grl2lnt
,
and lnt.open
. See grl2lnt
, lnt.open
for more information.
- -verbose
- Report activities and progress, including errors, to the user's
screen. This is the opposite of -silent. The default option is -verbose. This
option is passed to grl2lnt
, and lnt.open
. See grl2lnt
,
lnt.open
for more information.
- -version
- Display the version number
of grl2lnt
and stop.
- -about
- Display information about grl.open
and stop.
- -ignore
- Do not stop execution after an error is issued, force
the generation of an LNT file (possibly with errors). This option is passed
to grl2lnt
. See grl2lnt
for more information.
- -warnings
- Stop
execution when a warning is issued in GRL specification and exit with
status 1. This option is passed to grl2lnt
. See grl2lnt
for
more information.
- -merge
- Use merge mode. It simulates the merge of transitions
with adding a special merged transition and hiding everything else. This
option is passed to grl2lnt
. See grl2lnt
for more information.
- -sync
- Use synchronous mode. It enables the generation of merged transitions.
The option should be used only on synchronous programs. This option is passed
to grl2lnt
. See grl2lnt
for more information.
- -warning
- No warning
is issued in the GRL specification. This option is passed to grl2lnt
,
and lnt.open
. See grl2lnt
, lnt.open
for more information.
- -showall
- Show all transitions. This option is passed to grl2lnt
. See
grl2lnt
for more information.
- -force
- Overwrite output files, even
if they were edited by the user or do not need to be updated. This option
is passed to grl2lnt
, and lnt.open
. See grl2lnt
, lnt.open
for more information.
- -relabel
- Generate a rename file to match formal definition
of LTS labels (required by other tools). This option is passed to grl2lnt
.
See grl2lnt
for more information.
- -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. This option is passed to grl2lnt
, and lnt.open
.
See grl2lnt
, lnt.open
for more information.
- -labels
- Display
on user's screen the list of labels expected to be printed in the LNT specification
and for example on the generated LTS.
- lnt_options
- if any, are passed to
lnt.open
.
- cc_options
- if any, are passed to the C compiler.
- user_options
- if any, are passed to user.
- filename.grl
- GRL specification (input)
- pp_file.grl
- GRL code (optional output)
- filename.o
- object code (output)
- filename.err
- detailed error messages (output)
- user.a
- exploration module (archive, input)
- user.c
- exploration module (source, input)
- user.o
- exploration module (object
code, input)
- user
- executable program (output)
- $CADP_TMP/lnt.*
- temporary
files
- $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
,
grl2lnt
, 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.
Please report any bug to cadp@inria.fr
Table of Contents