BCG_MERGE manual page
Table of Contents

Name

bcg_merge - translation of a partitioned BCG graph into one single BCG graph

Synopsis

bcg_merge [options] input[.pbg] [output[.bcg]] [global_opt] [instance_opt]

Description

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 pbg 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 gcf 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.

Options

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 partitioned 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.

Environment Variables

See the bcg manual page for a description of the environment variables used by all BCG application tools.

Exit Status

Exit status is 0 if everything is alright, 1 otherwise.

Authors

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.

Operands

input.pbg
partitioned BCG graph (input)

output.bcg
resulting BCG file after merging (output)

Files

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.

See Also

bcg , gcf , pbg , distributor , pbg_cp , pbg_info , pbg_mv , pbg_rm

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.

Bugs

Please report bugs to cadp@inria.fr

Bibliography

[GMS01] Hubert Garavel, 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'01), Toronto, Canada, LNCS 2057, pp. 217-234, May 2001. Revised version available as INRIA Research Report RR-4341, December 2001. Available from http://cadp.inria.fr/publications/Garavel-Mateescu-Smarandache-01.html

[GMB+06] Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, and Gilles Stragier. DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation. In Holger Hermanns and Jens Palberg, eds., Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), Vienna, Austria, LNCS 3920, pp. 445-449, March-April 2006. Available from http://cadp.inria.fr/publications/Garavel-Mateescu-Bergamini-et-al-06.html

[GMS12] Hubert Garavel, Radu Mateescu, and Wendelin Serwe. Large-scale Distributed Verification using CADP: Beyond Clusters to Grids. Electronic Notes in Theoretical Computer Science, vol. 296, pp. 145-161, August 2012. Available from http://cadp.inria.fr/publications/Garavel-Mateescu-Serwe-12.html

Table of Contents