Table of Contents
generator - BCG graph generation using reachability analysis
bcg_open
[
bcg_opt]
spec[
.bcg] [
cc_opt]
generator [
generator_opt]
result[
.bcg]
or:
caesar.open [caesar_opt] spec[.lotos] [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:
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 LOTOS program
spec.lotos, the composition expression
spec.exp, the FSP program
spec.lts, the LOTOS NT program
spec.lnt, 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 caesar_opt, if any, are
passed to caesar
and to caesar.adt
.
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 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.
- -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.lotos
- LOTOS specification (input)
- spec.lts
- FSP specification
(input)
- spec.lnt
- LOTOS NT 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.
CAESAR
Reference Manual, OPEN/CAESAR Reference Manual,
bcg_open
,
bcg
,
caesar.open
,
caesar
,
caesar.adt
,
exp.open
,
fsp.open
,
lnt.open
,
seq.open
Additional information is available from
the CADP Web page located at http://cadp.inria.fr
Directives for installation
are given in file $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
