Table of Contents
bcg, BCG - Binary Coded Graphs: binary file format for labelled transition
The acronym BCG
stands for B
raphs. 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 from higher-level models of concurrent systems.
other existing formats with similar purposes, the BCG format combines
- The BCG format is independent from any particular model-based
verification technique; it can be used either by tools performing graph
comparison and reduction modulo equivalence relations, or by tools checking
properties expressed in temporal logics. It can also be used in other contexts:
graph exploration, graph drawing, etc.
- The BCG format is independent from
the language used to describe the concurrent system to be analyzed. It was
designed so as to allow the representation of graphs generated from various
- The BCG format provides sophisticated mechanisms to
keep track of source-level information. This is especially useful, since
it is possible to establish a connection between the behaviour of a BCG
graph and the source program from which the BCG graph was generated.
BCG format uses a binary representation of the LTS together with ad-hoc
compression algorihms, leading to very compact files. Graphs with millions
of states and transitions can be represented using only a few megabytes
of disk space.
Moreover, the BCG format is supported by an efficient and
extensive software implementation, the BCG environment.
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):
- Edit PostScript files generated by bcg_draw
- Print information about BCG graphs
graphs from and to the BCG format
- Generate various kinds
of useful BCG graphs
- Hide/rename labels of graph encoded
to the BCG format
- Generate dynamic libraries for BCG graphs
- Minimize of normal, probabilistic, or stochastic BCG graphs
- Execute OPEN/CAESAR application programs on BCG graphs
- Perform steady-state analysis on Markov chains encoded
in the BCG format
- 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
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.
are currently several ways of generating a BCG file:
- The caesar
tool can generate a BCG graph corresponding to a LOTOS description.
application program can be used to translate an existing
graph into a BCG graph.
- The generator
of the OPEN/CAESAR environment can be used to generate a BCG graph.
If you want to create a BCG graph by yourself, please
consult the bcg_write
want to read a BCG graph by yourself, please consult the bcg_read
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.
contents of static libraries are undocumented and subject to future changes.
In order to access the informations contained in BCG files,
application programs have to generate various files containing compiled
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 email@example.com, firstname.lastname@example.org, 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.
variables are defined and used according to UNIX conventions: see the
commands of the UNIX shells sh
(1) and csh
(1), and also the
manual pages for environ
(3), and putenv
are taken into account by all application tools.
The following environment
variables are defined:
- 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_2 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.
- 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_''.
- 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
- 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.
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
Unless stated otherwise, general options can appear at any
place on the command-line when an application tool is invoked.
general options are currently available:
- 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.
- 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.
- Do not create the dynamic library if it already
exists in the current directory and if it is up-to-date. Default option.
- Remove the dynamic library after usage. Not a default option.
- -cc options
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.
- 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.
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.
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
Application tools share common conventions with respect
to diagnostics. Exit status is 0 if everything is alright, 1 otherwise.
Garavel (definition of the BCG format) and Renaud Ruffiot (implementation
of the BCG environment).
- BCG files
- *@1.o, *@2.o, etc.
- dynamic libraries
- include files
- C compiler shell
- various source files
- binary programs
- static libraries
- static libraries
- temporary files
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 bugs
Table of Contents