|
| 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:
exp.open [exp_opt] spec[.exp] [cc_opt] determinator [determinator_opt] result[.bcg]
or:
fsp.open [fsp_opt] spec[.lts] [cc_opt] determinator [determinator_opt] result[.bcg]
or:
lnt.open [lnt_opt] spec[.lnt] [cc_opt] determinator [determinator_opt] result[.bcg]
or:
lotos.open [lotos_opt] spec[.lotos] [cc_opt] determinator [determinator_opt] result[.bcg]
or:
seq.open [seq_opt] spec[.seq] [cc_opt] determinator [determinator_opt] result[.bcg]
Extended Markovian models are state-transition models containing ordinary, probabilistic and/or stochastic transitions. Stochastic determinization consists in trying to convert the extended Markovian model spec into a continuous-time Markov chain (CTMC) by removing local sources of nondeterminism. It might fail if spec does not satisfy certain conditions. If it succeeds, the CTMC is written to result.bcg; otherwise, an error message is issued. See section STOCHASTIC DETERMINIZATION below for details.
Note: Since March 2006, determinization of ordinary Labelled Transition Systems is no longer supported by determinator. Option -rate becomes the default option. The formerly available options -normal and -tauclosure are now deprecated. Use the reductor tool instead, as explained below.
The options exp_opt, if any, are passed to exp.open .
The options fsp_opt, if any, are passed to fsp.open .
The options lnt_opt, if any, are passed to lnt.open .
The options lotos_opt, if any, are passed to caesar and to caesar.adt .
The options seq_opt, if any, are passed to seq.open .
The options cc_opt, if any, are passed to the C compiler.
The following options determinator_opt are currently available:
%f and %p mentioned in section STOCHASTIC
DETERMINIZATION below). The value of format_string should obey the same
conventions as the format parameter of function sprintf(3C) for values
of type double. Default value for format_string is "%g", meaning that floating-point
numbers are printed with at most six digits after the "." (i.e., the radix
character). Other values can be used, for instance "%.9g" to obtain nine
digits instead of six, or by replacing the "%g" flag with other flags,
namely "%e", "%E", "%f", or "%G", possibly combined with additional flags
(e.g., to specify precision).
The -total, -partial, and -gate options specify the "total matching", "partial matching", and "gate matching" semantics, respectively. See the caesar_hide_1 manual page for more details about these semantics. Option -total is the default.
The -total, -single, -multiple, and -gate options specify the "total matching", "single partial matching", "multiple partial matching", and "gate matching" semantics, respectively. See the caesar_rename_1 manual page for more details about these semantics. Option -total is the default.
As for the bcg_labels tool, several hiding and/or renaming options can be present on the command line, in which case they are processed from left to right.
rate %f" (called a stochastic transition), or ; rate %f" (called
a labelled stochastic transition), or prob %p" (called a probabilistic
transition), or ; prob %p" (called a labelled probabilistic transition),
or
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").
On the opposite, the expected output of determinator is a continuous-time Markov chain, i.e., a model containing stochastic transitions only.
See also bcg_min for a discussion about the various probabilistic and stochastic models present in the literature.
States are classified as follows:
Note: the bcg_steady and bcg_transient tools rely on the same notions of vanishing and tangible states, but do not have to consider decision states as they do not accept ordinary transitions.
In order to be accepted by determinator, the input model must satisfy two conditions (otherwise, determinator will emit an error message and stop):
Note that if there exists an ordinary transition or a (labelled) probabilistic transition from a state S1 to a state S2, then all (labelled) stochastic transitions from S1, if any, are discarded, thus expressing that ordinary and probabilistic transitions are instantaneous.
Note: The sum of %p values on (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) during determinization.
The stochastic determinization algorithm used
in determinator is a variant of Deavours-Sanders' algorithm [DS99]. In a nutshell,
it starts from the initial state of the input model and recursively explores
tangible states as follows. When in a tangible state S1, the algorithm inspects
all states S2 reachable from S1 by following one single (labelled) stochastic
transition, the rate of which will be noted %f:
%p to reach S3 from S2 does not depend on the choice
of the ordinary transitions followed. If so, a new stochastic transition
from S1 to S3 with rate %p*%f is added to result.bcg, and S3 will be explored
recursively. If not, determinator stops with an error message.
Note: if the initial state S0 is not tangible, and if one single tangible state S is reachable from S0 by following ordinary and/or probabilistic transitions only, then S will form the initial state of result.bcg. Otherwise, for each tangible state S reachable from S0 by following ordinary and/or probabilistic transitions only, a probabilistic transition from S0 to S (labelled with the probability to reach S) will be created; this is the only case where result.bcg will contain a vanishing state, i.e., the only case where determinator does not produce a continuous-time Markov chain, strictly speaking.
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.
[DS99] D. Deavours and W. Sanders. An Efficient Well-Specified Check. In Proceedings of the International Workshop on Petri Nets and Performance Models (PNPM'99), pages 124-133. IEEE Computer Society Press, 1999.
[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