Table of Contents
generator - BCG graph generation using reachability analysis
bcg_open
[
bcg_opt]
spec[
.bcg] [
cc_opt]
generator [
generator_opt]
result[
.bcg]
or:
exp.open [exp_opt] spec[.exp] [cc_opt] generator [generator_opt] result[.bcg]
or:
fsp.open [fsp_opt] spec[.lts] [cc_opt] generator [generator_opt] result[.bcg]
or:
lnt.open [lnt_opt] spec[.lnt] [cc_opt] generator [generator_opt] result[.bcg]
or:
lotos.open [lotos_opt] spec[.lotos] [cc_opt] generator [generator_opt]
result[.bcg]
or:
seq.open [seq_opt] spec[.seq] [cc_opt] generator [generator_opt]
result[.bcg]
This program performs exhaustive reachability analysis
and generates the Labelled Transition System corresponding to the BCG
graph
spec.bcg, the composition expression
spec.exp, the FSP program
spec.lts,
the LNT program
spec.lnt, the LOTOS program
spec.lotos, or the sequence file
spec.seq.
The resulting Labelled Transition System is encoded in the BCG
format and stored into file result.bcg.
Note: In its first form (i.e., when
applied to the BCG graph spec.bcg), this program is not very useful, since
the graph has already been generated.
The options
bcg_opt, if any,
are passed to
bcg_lib
.
The options exp_opt, if any, are passed to
exp.open
.
The options fsp_opt, if any, are passed to fsp.open
.
The options lnt_opt, if any, are passed to lnt.open
.
The options lotos_opt,
if any, are passed to caesar
and to caesar.adt
.
The options
seq_opt, if any, are passed to seq.open
.
The options cc_opt, if any,
are passed to the C compiler.
The following options generator_opt are currently
available:
- -monitor
- Open a window for monitoring in real-time the generation
of result.bcg.
- -hide [ -total | -partial | -gate ] hiding_filename
- Use the hiding
rules defined in hiding_filename to hide (on the fly) the labels of the
Labelled Transition System being generated. See the caesar_hide_1
manual page for a detailed description of the appropriate format for hiding_filename.
The -total, -partial, and -gate options specify the "total matching", "partial
matching", and "gate matching" semantics, respectively. See the caesar_hide_1
manual page for more details about these semantics. Option -total is the
default.
- -rename [-total|-single|-multiple|-gate] renaming_filename
- Use the renaming
rules defined in renaming_filename to rename (on the fly) the labels of
the Labelled Transition System being generated. See the caesar_rename_1
manual page for a detailed description of the appropriate format for renaming_filename.
The -total, -single, -multiple, and -gate options specify the "total matching",
"single partial matching", "multiple partial matching", and "gate matching"
semantics, respectively. See the caesar_rename_1
manual page for
more details about these semantics. Option -total is the default.
As for
the bcg_labels
tool, several hiding and/or renaming options can
be present on the command line, in which case they are processed from left
to right.
- -uncompress, -compress, -register, -short, -medium, -size
- These options
control the form under which the BCG graph result.bcg is generated. See
the bcg
manual page for a description of these options.
- -unparse,
-parse
- These options control label parsing when the BCG graph result.bcg
is generated. Default option is -parse. See the bcg_write
manual page
for a description of label parsing.
- -tmp
- This option specifies the directory
in which temporary files are to be stored. See the bcg
manual page
for a description of this option.
Exit status is 0 if everything
is alright, 1 otherwise.
When the source is erroneous, error
messages are issued.
Hubert Garavel (INRIA Rhone-Alpes)
- spec.bcg
- BCG graph (input)
- spec.exp
- network of communicating LTSs (input)
- spec.lts
- FSP specification (input)
- spec.lnt
- LNT specification (input)
- spec.lotos
- LOTOS
specification (input)
- spec.seq
- sequence file (input)
The source code
of this tool is available in file
$CADP/src/open_caesar/generator.c
See
the caesar_hide_1
, caesar_rename_1
, bcg_labels
manual
pages for a description of hiding and renaming conventions.
OPEN/CAESAR
Reference Manual,
bcg
,
bcg_open
,
caesar
,
caesar.adt
,
exp
,
exp.open
,
fsp.open
,
lnt.open
,
lotos
,
lotos.open
,
seq
,
seq.open
Additional information is
available from the CADP Web page located at http://cadp.inria.fr
Directives
for installation are given in files $CADP/INSTALLATION_*.
Recent changes
and improvements to this software are reported and commented in file $CADP/HISTORY.
Please report new bugs to
Hubert.Garavel@inria.fr
Table of Contents