BCG manual page
Table of Contents

Name

bcg, BCG - Binary Coded Graphs: universal graph format

Description

The acronym BCG stands for Binary Coded Graphs. It refers both to a format and a software environment.

The BCG format is a computer representation for labelled transition systems, Kripke structures, and, more generally, state/transition models (hereafter called graphs) which are generated for the modelling of concurrent systems. The BCG format is expected to become a common format for model-based verification tools.

The formal definition of the BCG format is given in an INRIA Technical Report (in preparation).

Compared to other existing formats with similar purposes, the BCG format combines several advantages:

Moreover, the BCG format is supported by an efficient and extensive software implementation, the BCG environment.

Application Tools

In the BCG environment, the programs dealing with graphs encoded in the BCG format are called ``application tools''. These programs can be either binary programs or shell-scripts.

The following application tools are currently available (see the corresponding manual pages):

bcg_draw
Display BCG graphs

bcg_edit
Edit PostScript files generated by bcg_draw

bcg_info
Print information about BCG graphs

bcg_io
Convert graphs from and to the BCG format

bcg_graph
Generate various kinds of useful BCG graphs

bcg_labels
Hide/rename labels of graph encoded to the BCG format

bcg_lib
Generate dynamic libraries for BCG graphs

bcg_min
Minimize of normal, probabilistic, or stochastic BCG graphs

bcg_open
Execute OPEN/CAESAR application programs on BCG graphs

bcg_steady
Perform steady-state analysis on Markov chains encoded in the BCG format

bcg_transient
Perform transient analysis on Markov chains encoded in the BCG format

Application Programming Interfaces for reading and/or writing BCG files from C or C++ programs are described in the bcg_read and bcg_write manual pages.

BCG Files

Graphs encoded in the BCG format are stored in files having the .bcg suffix. These files contain binary data, which are not directly readable by the user.

There are currently several ways of generating a BCG file:

How to Create a BCG Graph

If you want to create a BCG graph by yourself, please consult the bcg_write manual page.

How to Read a BCG Graph

If you want to read a BCG graph by yourself, please consult the bcg_read manual page.

Static Libraries

Application tools rely on libraries of compiled object code provided with the BCG environment. These libraries are called ``static libraries''. They are not directly visible by the user.

Caution: the contents of static libraries are undocumented and subject to future changes.

Dynamic Libraries

In order to access the informations contained in BCG files, application programs have to generate various files containing compiled object code.

These files are called ``dynamic libraries'' since they depend on BCG files to be accessed, which is not the case of ``static libraries''.

For a given BCG file filename.bcg, the corresponding dynamic libraries are files named filename@1.o, filename@2.o, etc. They are stored in the same directory as the BCG file itself.

Dynamic libraries can be safely removed: if they are necessary, they will be generated again by application tools. However, it is advised not to delete them systematically, since their generation takes a certain amount of time.

Caution: the contents of dynamic libraries are undocumented and subject to future changes.

Environment Variables

Environment variables are defined and used according to UNIX conventions: see the set and unset commands of the UNIX shells sh(1) and csh(1), and also the manual pages for environ(5), getenv(3), and putenv(3).

Environment variables are taken into account by all application tools.

The following environment variables are defined:

$CADP_CC
If this variable is set, its value determines the name of the C compiler that will be invoked by application tools. See file $CADP/INSTALLATION for detailed information about this variable. If this variable is unset, the script-shell $CADP/src/com/cadp_cc will automatically determine the C compiler to be used by default.

$CADP_TMP
If this variable is set, its value determines the directory in which temporary files will be created by application tools. If this variable is unset, it is given the default value '/tmp'. The names of temporary files are always be prefixed with the string ``bcg_''.

$BCG      
If this variable is set, its value should reference the directory in which the BCG package is installed. By default, this variable is supposed to be unset: the BCG package is normally installed in the directory referenced by the environment variable $CADP. Setting this variable should be avoided in official distributions of the BCG package, since it may cause problems.

$BCG_DEBUG
If this variable is set, diagnostic messages (which can be helpful in debugging) are displayed on the standard error stream. By default, this variable is supposed to be unset. Setting this variable has no effect in official distributions of the BCG package.

General Options

There exist command-line options which are common to many, if not all, application tools. Their meaning is the same in all the applications tools that support these options.

Unless stated otherwise, general options can appear at any place on the command-line when an application tool is invoked.

The following general options are currently available:

-version
Display the current version number of the application tool and stop. To be effective, this option should occur as the first argument on the command line. Subsequent options, if any, will be discarded.

-create
Force the dynamic library to be created, even if it already exists in the current directory and if it is up-to-date. Not a default option.

-update
Do not create the dynamic library if it already exists in the current directory and if it is up-to-date. Default option.

-remove
Remove the dynamic library after usage. Not a default option.

-cc options
Pass options to the C compiler when creating dynamic libraries. options is a list of compiler options (enclosed in quotes or double quotes). These options are appended to the compiler options, if any, contained in the $CADP_CC environment variable (see ENVIRONMENT VARIABLES below). Not a default option.

-tmp directory
Use directory to store temporary files. If present, this option overrides the environment variable $CADP_TMP.

-uncompress
Represent the edges of the graph using an edge area of code 1. This option is only meaningful when a BCG graph is to be created. Not a default option.

-compress
Represent the edges of the graph using an edge area of code 2. This option is only meaningful when a BCG graph is to be created. Default option.

-register register_size
Use register_size bits to encode registers offsets. This option is only meaningful when a BCG graph is to be created with an edge area of code 2. By default, register_size is equal to 4.

-short short_size
Use short_size bits to encode short branch offsets. This option is only meaningful when a BCG graph is to be created with an edge area of code 2. By default, short_size is equal to 1.

-medium medium_size
Use medium_size bits to encode medium offsets. This option is only meaningful when a BCG graph is to be created with an edge area of code 2. By default, medium_size is equal to 3.

-size register_size short_size medium_size
This option is equivalent to the simultaneous occurrence of the three following options: -register register_size, -short short_size, and -medium medium_size.

Particular Options

Besides general options, application tools can also accept their own options, which are not shared with other application tools. These particular options will be described in the manual pages of each application tools.

Diagnostics

Application tools share common conventions with respect to diagnostics. Exit status is 0 if everything is alright, 1 otherwise.

Authors

Hubert Garavel (definition of the BCG format) and Renaud Ruffiot (implementation of the BCG environment).

Files

*.bcg      
BCG files

*@1.o, *@2.o, etc.
dynamic libraries

$CADP/incl/bcg_*
include files

$CADP/com/bcg_*
shell-scripts

$CADP/src/com/cadp_cc
C compiler shell

$CADP/src/*/*
various source files

$CADP/bin.`arch`/bcg_*
binary programs

$CADP/bin.`arch`/libbcg_*.a
static libraries

$CADP/bin.`arch`/libBCG_*.a
static libraries

$CADP_TMP/bcg_*
temporary files

See Also

bcg_draw , bcg_edit , bcg_graph , bcg_info , bcg_io , bcg_lib , bcg_min , bcg_open , bcg_read , bcg_steady , bcg_transient , bcg_write .

Additional information is available from the CADP Web page located at http://www.inrialpes.fr/vasy/cadp

Directives for installation are given in file $CADP/INSTALLATION.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.

Bugs

Please report bugs to Hubert.Garavel@inria.fr

Table of Contents