DETERMINATOR manual page
Table of Contents

Name

determinator - elimination of nondeterminism for stochastic systems

Synopsis

bcg_open [bcg_opt] spec[.bcg] [cc_opt] determinator [determinator_opt] result[.bcg]

or:

caesar.open [caesar_opt] spec[.lotos] [cc_opt] determinator [determinator_opt] result[.bcg]

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:

seq.open [seq_opt] spec[.seq] [cc_opt] determinator [determinator_opt] result[.bcg]

Description

Taking as input an extended Markovian model expressed either as a BCG graph spec.bcg, a LOTOS program spec.lotos, a composition expression spec.exp, an FSP program spec.lts, a LNT program spec.lnt, or a sequence file spec.seq, determinator generates a reduced model by removing stochastic nondeterminism on-the-fly.

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.

Options

The options bcg_opt, if any, are passed to bcg_lib .

The options caesar_opt, if any, are passed to caesar and to caesar.adt .

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:

-epsilon eps
Set the precision of certain floating-point comparisons to eps, where eps is a real value. When eps is out of [0..1[, determinator reports an error. Default value for eps is 1E-6.

-format format_string
Use format_string to control the format of the floating-point numbers contained in transition labels (these numbers correspond to the occurrences of %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).

-hide [ -total | -partial | -gate ] hiding_filename
Use the hiding rules defined in hiding_filename to hide (on the fly) the labels of the CTMC being generated. See the caesar_hide_1 manual page for a detailed description of the appropriate format for hiding_filename.

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.

-rename [-total|-single|-multiple|-gate] renaming_filename
Use the renaming rules defined in renaming_filename to rename (on the fly) the labels of the CTMC being generated. See the caesar_rename_1 manual page for a detailed description of the appropriate format for renaming_filename.

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.

-monitor
Open a window for monitoring in real-time the generation of result.bcg. Not a default option.

-uncompress, -compress, -register, -short, -medium, -size
These options control the form under which the BCG graph result.bcg is generated. See the bcg manual page for a description of these options.

-tmp
This option specifies the directory in which temporary files are to be stored. See the bcg manual page for a description of this option.

Deprecated Options

-rate
This option is supported for backward compatibility but has no effect.

-normal
This option triggers an error message. Use ``reductor -trace'' instead of ``determinator -normal''.

-tauclosure
This option triggers an error message. Use ``reductor -weaktrace'' instead of ``determinator -normal -tauclosure''.

Stochastic Determinization

The input of determinator is an extended Markovian model combining features from discrete-time and continuous-time Markov chains. All transition labels must have one of the following forms:

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:

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.

Exit Status

Exit status is 0 if everything is alright, 1 otherwise.

Diagnostics

When the source is erroneous, error messages are issued.

Authors

The first version of the stochastic determinization was written by Christophe Joubert (INRIA/VASY) and Holger Hermanns (Saarland University and University of Twente). Frederic Lang (INRIA/VASY) deeply revised the code. Frederic Lang and Hubert Garavel (both at INRIA/VASY) wrote the current determinator manual page.

Operands

spec.bcg
BCG graph (input)

spec.exp
network of communicating LTSs (input)

spec.lotos
LOTOS specification (input)

spec.lts
FSP specification (input)

spec.lnt
LNT specification (input)

spec.seq
SEQ file (input)

result.bcg
BCG graph (output)

See Also

OPEN/CAESAR Reference Manual, bcg , bcg_min , bcg_open , bcg_steady , bcg_transient , caesar.open , caesar , caesar.adt , exp.open , fsp.open , lnt.open , seq.open , sprintf(3C)

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.

Bugs

Please report bugs to cadp@inria.fr

Bibliography

[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


Table of Contents