Table of Contents
bcg_merge - translation of a partitioned BCG graph into one single
BCG graph
bcg_merge [
options]
input[.pbg] [
output[
.bcg]] [
global_opt]
[
instance_opt]
bcg_merge is usually invoked after the
distributor
tool of
CADP for distributed state-space generation.
bcg_merge takes as input
a partitioned BCG graph input[.pbg], usually produced by distributor
and encoded in the PBG format (see the distributor
manual page for
details about the PBG format), and produces one single BCG file output[.bcg]
that combines the various graph fragments listed in input[.pbg].
If output[.bcg]
is not specified on the command line, the output file will be named input.bcg.
These graph fragments are themselves encoded as BCG files and usually located
on different machines. The list of these machines is given in a grid configuration
file (see the distributor
manual page for details about the GCF
format) referenced in input[.pbg].
bcg_merge renumbers the states contained
in the BCG files listed in the input PBG file, in such a way that the states
of the output BCG file are assigned contiguous numbers and that the initial
state is assigned number 0.
The following
options are currently
supported:
- -compress, -register, -short, -medium, -size, -uncompress
- These options
control the form under which the BCG graph output.bcg is generated. See the
bcg
manual page for a description of these options.
- -clean
- After generating
the output BCG file, erase the input PBG file together with its BCG graph
fragments and their corresponding BCG dynamic libraries. Not a default option.
- -fast
- When building output[.bcg], sort, by increasing source state numbers
only, the transitions belonging to the file fragments listed in input[.pbg].
This is a faster sort than the default one, which sorts transitions lexicographically,
by increasing source state numbers, then by increasing target state numbers;
however, this faster sort may generate a larger BCG file than the lexicographic
sort. Not a default option.
- -monitor
- Open a window for monitoring in real-time
the generation of the BCG file output.bcg. Not a default option.
- -parse | -unparse
- These options can be used to control label parsing in the output BCG graph
(see the bcg_write
manual page for a technical discussion about
label parsing). By default, or if option -parse is present, label parsing
is enabled. If option -unparse is present, label parsing is disabled.
- -stat
- Display various statistics obtained during graph merging, such as the number
of cross-border transitions in the partitionned BCG graph, and the network
traffic with the remote machines. Not a default option.
- -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.
Finally, the list of options
global_opt and instance_opt can be used for last-minute changes to the
settings of the grid configuration file referenced in input[.pbg]. See the
distributor
manual page for a description of these options.
See the
bcg
manual page for a description of the environment
variables used by all BCG application tools.
Exit status is 0
if everything is alright, 1 otherwise.
Version 1.0 of
bcg_merge was
developed by Irina Smarandache-Sturm (INRIA/VASY) in 2000.
Version 2.0 of
bcg_merge was developed by Radu Mateescu (INRIA/VASY) in 2001.
Version
3.0 of bcg_merge was developed by Nicolas Descoubes (INRIA/VASY) in 2003,
then revised by Damien Bergamini and Hubert Garavel (both at INRIA/VASY)
in 2004.
- input.pbg
- partitioned BCG graph (input)
- output.bcg
- resulting
BCG file after merging (output)
The binary code of
bcg_merge is available
in $CADP/bin.`arch`/bcg_merge.
During the execution of bcg_merge, dynamic libraries
corresponding to the BCG files (i.e., the graph fragments) listed in the
input PBG file may be generated if necessary, and stored on the remote
machines.
bcg
,
distributor
Additional information
is available from the CADP Web page located at http://cadp.inria.fr
Please
report bugs to
cadp@inria.fr
[GMS01] Hubert Garavel and Radu
Mateescu and Irina Smarandache. Parallel State Space Construction for Model-Checking.
In Matthew B. Dwyer, ed, Proceedings of the 8th International SPIN Workshop
on Model Checking of Software SPIN'2001 (Toronto, Canada), LNCS 2057, pp.
217-234, May 2001. Revised version available as INRIA Research Report RR-4341,
December 2001.
Table of Contents
