|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
or
bcg_graph [bcg_options] -bag size [labelfile | -labels number pattern1 pattern2] [-monitor] [-verbose] output [.bcg]
or
bcg_graph [bcg_options] -fifo size [labelfile | -labels number pattern1 pattern2] [-monitor] [-verbose ] output [.bcg]
Note: Such particular graphs could be easily described in a high-level language such as LOTOS or LNT, and then translated to BCG. However, the bcg_graph tool contains specialized algorithms designed for time and memory efficiency and ensuring that each generated graph is minimal wrt to branching bisimulation.
Note: Unless specified otherwise, bcg_graph generates graphs that are minimal for strong equivalence (i.e., that do not contain redondant states or transitions). However, this property is only ensured if the specified labels are pairwise different.
A chaos automaton is determined by the number N (with N >= 0) of different messages it can handle. It has a single state and N looping transitions, each labelled by a different message.
A bag buffer is determined by its size P (with P >= 0), which is the maximal number of messages that can be stored into the buffer, and the number N (with N >= 0) of different messages (there are N labels corresponding to message inputs and N labels corresponding to message outputs; see the notions of get-label and put-label below).
The number of states of a bag buffer is equal to
(N+P)! / (N! * P!)The number of transitions of a bag buffer is equal to
if N=0 or P=0 then 0 else 2*(N+P-1)!/((N-1)!*(P-1)!)
A FIFO buffer is determined by its size P (with P >= 0), which is the maximal number of messages that can be stored into the buffer, and the number N (with N >= 0) of different messages (there are N labels corresponding to message inputs and N labels corresponding to message outputs; see the notions of get-label and put-label below).
The number of states of a FIFO buffer is equal to
sum_{k in 0..P} N^k
or also if N=1 then P+1 else (N^(P+1)-1)/(N-1)The number of transitions of a FIFO buffer is equal to
2 * N * sum_{k in 0..P-1} N^k
or also if N=1 then 2*P else 2*N*(((N^P)-1)/(N-1))
For some forms of graphs (such as -chaos), a single list of labels is needed.
For other forms of graphs (such as -bag and -fifo), two lists of labels are needed: the get-labels (corresponding to input messages) and the put-labels (corresponding to output messages). There is a pairwise correspondence between both lists, as each put-label emitted corresponds to a get-label received previously.
A labelfile
contains a list of labels separated with newline characters. Labels are
strings of characters without newline characters. Labels can be enclosed
between double quotes, which will be ignored, and may contain spaces. For
instance, A, "B", and "A !1 !CONS(3, 4)" are valid labels. In the label
definition file, lines that contain only spaces (including empty lines)
are ignored. On each line, leading and trailing spaces are ignored, unless
they are enclosed in quotes.
For graphs requiring two lists of labels, the position of each label in the file determines whether it is a put-label or a get-label. In the labelfile, pairs of corresponding labels alternate strictly. Each get-label occurs on an odd-numbered line and is followed by its corresponding put-label on an even-numbered line (empty lines notwithstanding). Therefore, there must be an even number of labels in labelfile.
The degenerate case in which labelfile contains no label (e.g., the file is empty) is permitted and no warning will be issued.
A pattern is a character string to be used as the format argument of the C function printf(). It should contain exactly one occurrence of "%d" (and no occurrence of other %-arguments such as "%c", "%f", etc.). If needed, the "%" character can be specified as "%%".
Patterns are used to generate labels, the "%d" argument being substituted by an integer in the range [1..number]. If number is null, the generated set of labels is empty.
For graphs requiring two lists of labels, pattern1 defines the get-labels and pattern2 defines the put-labels; each put-label is associated with the get-label instantiated with the same number.
bcg_graph -fifo 2 labelfile output.bcg'' will generate
a graph named output.bcg modeling a 2-place FIFO buffer whose get- and put-labels
are defined in labelfile. bcg_graph -chaos -labels 4 "A%d" output.bcg'' will
generate a graph named output.bcg consisting of a single state and four
transitions labeled A1 through A4. bcg_graph -bag 2 -labels 3 "GET \!%d" "PUT
\!%d" output.bcg'' will generate a graph named output.bcg modeling a 2-place
bag buffer whose labels are named GET !1, PUT !1, GET !2, PUT !2, GET !3,
and PUT !3 respectively. Note: the "!" characters are escaped with backslashes
in order to avoid problems with csh/tcsh history substitution features.
bcg_graph cannot generate graphs with more than 2^32 transitions (note that the number of transitions is always larger than the number of states).
Moreover, if the available memory is unsufficient, bcg_graph might be unable to generate large graphs (even with less than 2^32 transitions).
bcg_graph does not check if the specified labels are pairwise different.
See the bcg manual page for a description of the environment variables used by all the BCG application tools.
See the bcg manual page for a description of the other 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.