|
| 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 Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
where bcg_options is defined below (see GENERAL OPTIONS).
bcg_transient first transforms filename.bcg into a numerical matrix indexed by states. Then, it reduces this matrix by normalizing probabilistic transitions, removing unreachable states and "vanishing" states, keeping "tangible" states only (see section INPUT below for details about the BCG graphs accepted by bcg_transient and the definition of tangible and vanishing states). As a result, the reduced matrix obtained is the generator matrix of a continuous-time Markov chain. Finally, bcg_transient computes the time-dependent ("transient") probability distribution of the model at several (user-specified) time instants using the uniformization algorithm [Jen53] (and the Fox-Glynn method [FG88] to approximate Poisson probabilities). It can also compute throughputs for the transitions of the system.
The optional list of "parameter=value" arguments at the end of the command line (where parameter is any character string that neither contain blanks nor the "=" character, and where value is any character string that does not contain blanks) is only meaningful to option -thr. These arguments have no influence on the actual numerical computations, they only serve to add columns in throughput tables (see section OUTPUT-2 below).
Time is a special parameter that can be dealt with using the (optional)
argument "time=here", whose meaning is detailed in section OUTPUT-2 below.
When parameter is equal to "time", value must be equal to the keyword "here".
The time_instants are strictly positive real numbers, and there must be at least one time_instant.
The following options are supported:
The files solution_file, throughput_file, matrix_file, reduced_matrix_file, and log_file should be pairwise different; otherwise, the result is undefined.
rate %f" (called
a stochastic transition), ; rate %f" (called a labelled stochastic
transition), prob %p" (called a probabilistic transition), or ; prob
%p" (called a labelled probabilistic transition) ,
where %f denotes a strictly
positive floating-point number, %p denotes a floating-point number in the
range ]0..1], and label denotes a character string that does not contain
the ";" character (label may be equal to the internal action, often noted
"i" or "tau").
Note: transitions labelled with only "label" are always forbidden by bcg_transient, including the case where "label" denotes the internal action.
When constructing the "raw" matrix, all labels occurring in labelled probabilistic transitions are discarded.
If there exists a (labelled) probabilistic transition from a state S1 to a state S2, then all (labelled) stochastic transitions from S1 to any state (including S2) are discarded when constructing the "raw" matrix. This reflects that probabilistic transitions are instantaneous, while stochastic transitions are not.
We classify states as being either vanishing if at least one (possibly labelled) probabilistic transition goes out of these states, or tangible otherwise.
The input BCG graph should contain at least one tangible state, and it should not contain cycles of vanishing states connected by (possibly labelled) probabilistic transitions.
Note: The sum of %p values on all (possibly labelled) probabilistic
transitions leaving a vanishing state needs not be equal to 1; if this
sum is different from 1, then probabilistic values will be normalized (i.e.,
divided by this sum).
To build the reduced matrix, bcg_steady eliminates all vanishing states, so that this matrix contains tangible states only.
See also bcg_min for a discussion about the various probabilistic and stochastic models present in the scientific literature.
The throughput table has two (possibly empty) groups of columns:
time=here"
option, if present, since there is only one single column for time). These
columns, if any, are useful when evaluating the performance of a system
parameterized with one or more variables, namely to aggregate in the same
table the different throughputs measures corresponding to different time
instants and different values of the parameters. Columns of the first group
appear in the same order as the corresponding options on the command line.
By default, time appears in the first column, unless the "time=here" option
is present, in which case the time column appears at the place specified
by this option. ; rate %f".
The throughput table starts with a first "header" line followed by one or several "subsequent" lines.
time. For a column
of the second group associated to a label, the corresponding title is the
label itself. time the corresponding cell contains the value of t; otherwise,
the corresponding cell contains value, which is the same for all time instants.
For a column of the second group associated to a label, the corresponding
cell contains the throughput for this label at time t, i.e., the sum, for
each stochastic transition "label; rate %f", of the rate value %f weighted
with the probability of being in the tangible source state of this transition
at time t.
If the -append option is absent, or if the throughput file is equal to the special string `-', or if the throughput file does not exist, or if it is empty, bcg_transient will generate automatically the header line and the subsequent lines.
Otherwise, the first line of the throughput file is expected to contain the titles of columns and will be parsed to identify the correspondance between labels and columns. In particular, bcg_transient checks that the first group of columns corresponds to the parameters given on the command line. After parsing the header line, bcg_transient will append the subsequent lines at the end of the throughput file. As regards the second group of columns, if the label of a given column title does not occur in filename.bcg, a zero throughput will be reported in the corresponding column; conversely, labels of filename.bcg for which there is no corresponding column title will be ignored.
Throughputs can be displayed in two different formats, which are determined according to the suffix (i.e., file extension) of the throughput file name.
For two different indexes i and j, the element (i,j) of the matrix, located at the i-th row and the j-th column, is the sum of all the floating-point numbers associated to the (labelled) stochastic or probabilistic transitions going from the j-th state to the i-th state, where floating-point numbers associated to (labelled) stochastic transitions are interpreted as positive numbers whereas floating-point numbers associated to (labelled) probabilistic transitions are interpreted as negative numbers between -1 and 0. Note that rates and probabilities are never mixed since, between two states, there cannot be stochastic and probabilistic transitions at the same time.
The diagonal elements (i,i) are defined to be the negative sum of all matrix elements (i,j) with j different from i.
Matrices can be displayed in three different formats, which are determined according to the suffix (i.e., file extension) of the matrix file name.
real" keyword. Then, there is one line per each non-zero element (i,j)
in the matrix. Each line contains two integers followed by one real number:
the value of i, the value of j, and the value of matrix element (i,j). The
file ends with a "sentinel" line consisting of three zeros.
Note: for graphs with many states, whatever the chosen matrix format, the matrix files can be large and writing them to disk may take time.
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.
[FG88] B.L. Fox and P.W. Glynn. Computing Poisson probabilities. Communications of the ACM 31(4), 1998, pages 440-445.
[GH02] H. Garavel and H. Hermanns. On Combining Functional Verification and Performance Evaluation using CADP. In proceedings of FME'2002, LNCS 2391, pages 410-429, Springer Verlag. Full version available as INRIA Research Report 4492. Available from http://cadp.inria.fr/publications/Garavel-Hermanns-02.html
[HJ03] H. Hermanns and Ch. Joubert. A Set of Performance and Dependability Analysis Components for CADP. In proceedings of TACAS'2003, LNCS 2619, pages 425-430, Springer Verlag. Available from http://cadp.inria.fr/publications/Hermanns-Joubert-03.html
[Jen53] A. Jensen. Markov Chains as an Aid in the Study of Markov Processes. Skand. Aktuarietidskrift 3, pages 87-91, 1953.
[Mer98] V. Mertsiotakis. Approximate Analysis Methods for Stochastic Process Algebras. Ph.D Thesis, University of Erlangen (Germany).