exp.open [exp_opt] spec[.exp] [cc_opt] determinator [determinator_opt] result[.bcg]
fsp.open [fsp_opt] spec[.lts] [cc_opt] determinator [determinator_opt] result[.bcg]
lnt.open [lnt_opt] spec[.lnt] [cc_opt] determinator [determinator_opt] result[.bcg]
lotos.open [lotos_opt] spec[.lotos] [cc_opt] determinator [determinator_opt] result[.bcg]
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.bcg_lib .
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 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:
%pmentioned 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
"%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
%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
;" 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:
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
%pto 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
%fis 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.firstname.lastname@example.org
[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