Table of Contents
bcg_write - a simple interface to produce a BCG graph
This
interface generates a BCG graph from an application program written in
C or C++. To keep things simple, this interface does not give access to
the whole BCG format, but only to a subset, in which states are assumed
to be unsigned integer numbers and labels of the edges are assumed to be
character strings. Note: this subset of BCG is equivalent to the
.aut format
described in the
aldebaran
manual page, although it is much more
compact.
The application program should start with the following directive:
#include "bcg_user.h"
Then the BCG library should be initialized by invoking
the following function:
BCG_INIT ();
Not invoking this function might
cause a run-time error, e.g., a segmentation fault. Invoking BCG_INIT() more
than once is harmless, although not recommended.
The functions
of this interface use the followings types, whose definitions are provided
by the "bcg_user.h" file:
BCG_TYPE_BOOLEAN BCG_TYPE_NATURAL BCG_TYPE_C_STRING
BCG_TYPE_FILE_NAME BCG_TYPE_LABEL_STRING BCG_TYPE_STATE_NUMBER
BCG_TYPE_BOOLEAN BCG_IO_WRITE_BCG_BEGIN (filename,
initial_state, format, comment, monitor)
BCG_TYPE_FILE_NAME filename;
BCG_TYPE_STATE_NUMBER initial_state;
BCG_TYPE_NATURAL format;
BCG_TYPE_C_STRING comment;
BCG_TYPE_BOOLEAN monitor;
{ ... }
This function opens a BCG file. Its arguments have the following meaning:
- filename
- is a character string containing the path name of the BCG file
to be written. It should contain the "
.bcg" suffix (if the ".bcg" suffix
is missing, it will be added automatically).
- initial_state
- is the number
of the initial state (usually 0).
- format
- is equal to 2 if, in the forthcoming
successive invocations of function
BCG_IO_WRITE_BCG_EDGE(), the sequence
of actual values given to the state1 argument of BCG_IO_WRITE_BCG_EDGE()
will increase monotonically or equal to 1 otherwise. The format 1 applies
in general but is less efficient in terms of time or BCG file compression.
The format 2 is more efficient but only applies to specific situations
(in particular, when the BCG graph is generated in a breadth-first search).
- comment
- is a character string containing information about the application
tool which is creating the BCG graph. If comment is equal to NULL, then
it will be replaced with a default string.
- monitor
- should be equal to
BCG_TRUE
if a Tcl/Tk window should be opened for monitoring in real-time the generation
of the BCG graph or equal to BCG_FALSE otherwise.
By default, if filename
cannot be opened for writing, BCG_IO_WRITE_BCG_BEGIN() will emit an error
message and exit the program. However, if the following function call:
BCG_IO_WRITE_BCG_SURVIVE (BCG_TRUE);
has occured before the call to
BCG_IO_WRITE_BCG_BEGIN(), then BCG_IO_WRITE_BCG_BEGIN() will neither emit
an error message nor exit the program, but return normally a boolean result
that is equal to BCG_TRUE if and only if filename cannot be opened.
Below,
we assume that the BCG_IO_WRITE_BCG_BEGIN() function has returned successfully.
BCG_IO_WRITE_BCG_SURVIVE (mode)
BCG_TYPE_BOOLEAN mode;
{ ... }
This function controls how the
BCG_IO_WRITE_BCG_BEGIN() function defined
above will behave if the BCG file cannot be opened for writing:
- If mode
equals
BCG_FALSE, then BCG_IO_WRITE_BCG_BEGIN() will emit an error message
and exit the program. This is the default behaviour. - If mode equals
BCG_TRUE,
then BCG_IO_WRITE_BCG_BEGIN() will neither emit an error message nor exit
the program, but return a boolean result. The default behaviour can be
restored by calling:
BCG_IO_WRITE_BCG_SURVIVE (BCG_FALSE);
BCG_IO_WRITE_BCG_EDGE (state1, label, state2)
BCG_TYPE_STATE_NUMBER state1;
BCG_TYPE_LABEL_STRING label;
BCG_TYPE_STATE_NUMBER state2;
{ ... }
This function must be invoked once for each edge to be created in the BCG
graph. It writes in the previously opened BCG file an edge such that
state1
is the number of the origin state,
state2 is the number of the destination
state, and
label is a character string containing the label.
Note: label
should not contain the characters newline ('\n') or carriage return ('\r').
Note:
the invisible (also known as hidden, or tau) label is represented by the
character string "i" (as it is the case in LOTOS).
BCG_IO_WRITE_BCG_PARSING (parsing_mode)
BCG_TYPE_NATURAL parsing_mode;
{ ... }
Calling
BCG_IO_WRITE_BCG_PARSING() with the
parsing_mode argument set to
0 turns off the parsing of labels, which is normally enabled by default.
For more details read the
TECHNICAL NOTE ON LABEL PARSING section below.
The call to BCG_IO_WRITE_BCG_PARSING() must be done after invoking BCG_INIT()
and before invoking BCG_IO_WRITE_BCG_BEGIN().
BCG_IO_WRITE_BCG_END ()
{ ... }
This function closes the BCG file.
The following piece of C code creates a BCG graph with an initial
state numbered 0:
#include "bcg_user.h"
int main ()
{
BCG_TYPE_STATE_NUMBER S1;
BCG_TYPE_LABEL_STRING L;
BCG_TYPE_STATE_NUMBER S2;
BCG_INIT ();
BCG_IO_WRITE_BCG_BEGIN ("test.bcg", 0, 2, "created by tool", 1);
/* for each transition labelled with L from state S1 to state S2 */
{
BCG_IO_WRITE_BCG_EDGE (S1, L, S2);
}
BCG_IO_WRITE_BCG_END ();
return (0);
}
By default, the character strings passed
to the function
BCG_IO_WRITE_BCG_EDGE() (i.e., all the 2nd arguments passed
to this function) are assumed to follow the LOTOS syntax for labels, i.e.,
"G !V1 !V2 ... !Vn", where G is a gate identifier and V1, V2, ..., Vn are values.
By default, when generating the BCG file, the function BCG_IO_WRITE_BCG_EDGE()
will attempt to parse the character strings passed to it, so that, in the
BCG file, the labels will be represented as tuples (G, V1, V2, ..., Vn).
Moreover,
in this case, the function BCG_IO_WRITE_BCG_EDGE() will attempt to perform
some (limited) inference of the types contained in the labels:
- The first
field G of each tuple is assumed to belong to be a value of an enumerated
"gate" type that contains all the gate identifiers contained in the labels
of the graph.
For the remaining fields V1, V2, ..., Vn:
- Sub-strings denoting
integer values (e.g., 0, 1, 9999, etc.) are recognized and implemented as
integer values in the BCG file. The syntax accepted for integer values
is the one accepted by the C library function strtol(3).
- Sub-strings denoting
real values (e.g., 3.14, 1.2E+10, etc.) are recognized and implemented as real
values in the BCG file. The syntax accepted for real values is the one
accepted by the C library function strtod(3).
- Sub-strings equal to "
TRUE"
or "FALSE" (as well as case-insentive variants such as "true", "false",
"True", "False", etc.) are recognized and implemented as boolean values
in the BCG file. - Sub-strings that do not match the above cases are implemented
as character strings in the BCG file.
Label parsing is especially of interest
when using the XTL model-checker, which takes advantage of the types and
typed values defined in BCG files.
However, for other tools operating on
the BCG format than XTL (e.g., bcg_draw
and bcg_edit
, for instance),
label parsing should be fully transparent, because these tools convert
the label tuples contained in the BCG file into character strings (thus
loosing all type information).
Therefore, even if the labels of the BCG
graph to be generated do not follow the LOTOS syntax for labels, label
parsing should have no visible effect for the user.
In some cases, however,
some form of "label normalization" can take place. For instance, if the
following character string "G !true ! 003 !+01E+0" is passed to function
BCG_IO_WRITE_BCG_EDGE(), it will be understood and stored in the BCG file
as the tuple (G, TRUE, 3, 1.0). Then, the BCG tools will usually convert
this label to the following character string "G !TRUE !3 !1.000000". Therefore,
"label normalization" can remove redundant spaces, leading zeros in integer
and real numbers, add trailing zeros to real numbers, and convert boolean
constant to upper-case letters.
If absolutely necessary, the default behaviour
(i.e., label parsing) can be turned off by invoking the following function:
BCG_IO_WRITE_BCG_PARSING (0);
after the invocation of BCG_INIT() and
before invoking BCG_IO_WRITE_BCG_BEGIN(). This will have the effect of storing
each label in the generated BCG file as a 1-tuple (L) whose single field
L is exactly the character string passed to BCG_IO_WRITE_EDGE(). However,
in order to improve inter-operability between tools, we do not recommend
this practice.
To compile the application tool,
the following options must be passed to the C or C++ compiler:
-I$CADP/incl
-L$CADP/bin.`$CADP/com/arch` -lBCG_IO -lBCG -lm
as in, e.g.,
$CADP/src/com/cadp_cc tool.c -o tool -I$CADP/incl \
-L$CADP/bin.`$CADP/com/arch` -lBCG_IO -lBCG -lm
Application tools share common conventions with respect to diagnostics.
Exit status is 0 if everything is alright, 1 otherwise.
Hubert Garavel
(definition of the BCG format) and Renaud Ruffiot (implementation of the
BCG environment).
See the
bcg
manual page for a description
of the files.
bcg
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.
Please report bugs to
Hubert.Garavel@inria.fr
Table of Contents
