CUNCTATOR manual page
Table of Contents

Name

cunctator - on-the-fly steady-state simulation of continuous-time Markov chains

Synopsis

bcg_open [bcg_opt] spec[.bcg] [cc_opt] cunctator [cunctator_opt]

or:

caesar.open [caesar_opt] spec[.lotos] [cc_opt] cunctator [cunctator_opt]

or:

exp.open [exp_opt] spec[.exp] [cc_opt] cunctator [cunctator_opt]

or:

fsp.open [fsp_opt] spec[.lts] [cc_opt] cunctator [cunctator_opt]

or:

lnt.open [lnt_opt] spec[.lnt] [cc_opt] cunctator [cunctator_opt]

or:

seq.open [seq_opt] spec[.seq] [cc_opt] cunctator [cunctator_opt]

Description

cunctator (from the Latin, the one who temporises) takes as input a continuous-time Markov chain (CTMC), expressed either as a BCG graph spec.bcg, a LOTOS program spec.lotos, a composition expression spec.exp, an FSP program spec.lts, an LNT program spec.lnt, or a sequence file spec.seq.

cunctator performs an on-the-fly random simulation of the CTMC, by a forward traversal of a transition sequence in the CTMC, and computes, for certain specified transitions, their throughput at the equilibrium ("steady-state"). The simulation terminates either when some convergence criterion is met (see OPTIONS below), or when the user aborts it (e.g., by typing a Ctrl-C). Upon termination of the simulation, the values of the throughputs, accompanied by other simulation statistics, are displayed on standard output.

All transition labels of the CTMC must have one of the following forms:

where %f denotes a strictly positive floating-point number, and action denotes a character string that does not contain the ";" character.

If the graph specified by spec also contains transition labels of other forms than the aforementioned ones, these labels must be hidden or renamed using the -hide and the -rename options (see OPTIONS below) in order to turn spec into a CTMC.

A state is called stable if it has no outgoing internal transitions and is called unstable otherwise.

The simulation algorithm used by cunctator applies the notion of maximal progress: every time an unstable state is encountered, all its outgoing stochastic transitions are ignored and the simulation sequence is advanced along some of its outgoing internal transitions.

The CTMC is assumed not to contain nondeterminism, which means that all internal transitions going out of an unstable state must lead to states that are equivalent modulo stochastic branching bisimulation. For efficiency reasons, cunctator does not attempt to perform this check, but instead it displays among the simulation statistics whether potential nondeterminism was encountered or not, i.e., whether a state having at least two outgoing internal transitions was reached during simulation. The tool also offers several ways of choosing internal transitions by means of the -scheduler option (see OPTIONS below) in order to study whether they yield the same throughputs (which indicates the possible absence of nondeterminism) or not (which indicates the necessary presence of nondeterminism).

See also bcg_min for a discussion about the various probabilistic and stochastic models present in the literature.

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 cunctator_opt are currently available:

-action action_1 ... action_n
Specify the actions contained in the labels of stochastic transitions "action_i; rate %f" (for 1 <= i <= n) of the CTMC for which the throughput must be computed. All the stochastic transitions of the CTMC having labels other than "action_i; rate %f" (for 1 <= i <= n) are considered as purely stochastic transitions (i.e., their actions are ignored and only their rates are taken into account) during the simulation. If this option is absent, the throughput is computed for all the actions contained in the labels of stochastic transitions of the CTMC.

To obtain useful results, each of the actions action_i (for 1 <= i <= n) must be contained in the label of at least one stochastic transition of the CTMC. This can be ensured by taking care that the options -action, -hide, and -rename are compatible. If some action action_i is absent from the CTMC, its throughput will be always equal to 0.0 regardless of the other parameters of the simulation.

Note: For efficiency reasons, it is recommended to use this option whenever the actions for which the throughput must be computed are known.

-hide [ -total | -partial | -gate ] hiding_filename
Use the hiding rules defined in hiding_filename to hide (on-the-fly) the labels of spec. 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 spec. 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.

The hiding and renaming options are useful for converting the transition labels of spec on-the-fly in order to transform it into a CTMC. If (one of) these options and the -action option are present on the command-line, the hiding and renaming options will be applied before the -action option is taken into account.

-cache size repl
Trigger the use of an internal cache for storing at most size states in order to speed up simulation by avoiding the recomputation of certain sequences of internal transitions. When the cache is full and a new state must be inserted in it, some other state present in the cache is deleted and replaced by the new one. The choice of the state to be deleted is made according to the replacement strategy repl, which can take one of the following values: LRU (Least Recently Used), MRU (Most Recently Used), LFU (Least Frequently Used), MFU (Most Frequently Used), and RND (Random). This option can be used only for the schedulers 0 and 1 (see option -scheduler below). By default, the size of the cache is 0 (i.e., no caching is performed during simulation). Not a default option.

-depth depth
Specify the maximum number of transitions of the sequence traversed during simulation. When the number of transitions of the current simulation sequence becomes equal to the natural number depth, then the simulation terminates and the statistics are reported. A value 0 of depth means no limit, i.e., the simulation will run for ever unless aborted by the user. The default value of depth is 0.

-time time
Specify the maximum simulation time, which is the sum of all durations spent in the stable states of the transition sequence traversed during simulation. When the current simulation time (the sum of durations spent in the stable states of the current simulation sequence) becomes equal to or greater than the real number time, then the simulation terminates and the statistics are reported. A value 0.0 of time means no limit, i.e., the simulation will run for ever unless aborted by the user. The default value of time is 0.0.

If both options -depth and -time are present on the command-line, the option -depth is ignored in favor of -time.

-scheduler n
Specify the way an internal transition going out of an unstable state is chosen during simulation in order to apply the notion of maximal progress. When the current state has several outgoing internal transitions, choosing a particular one as the next transition to be traversed amounts to model a particular scheduler. The following values are currently available for the scheduler n:

- 0: Choose the first internal transition encountered while scanning the transitions going out from the current state.

- 1: Choose the last internal transition encountered while scanning the transitions going out from the current state.

- 2: Choose randomly (with equal probability) one of the internal transitions going out from the current state.

This option enables the user to experiment with several schedulers in order to study their effect on the throughputs computed by simulation. Several simulations differing only in the scheduler used and yielding the same throughputs indicate the possible absence of nondeterminism in the CTMC. Two simulations differing only in their scheduler and yielding different throughputs indicate the necessary presence of nondeterminism in the CTMC. The default value of n is 0.

-rng n
Specify the random number generator used for computing the current simulation time and to select the transitions of the simulation sequence. Four random number generators are currently available (n = 0, 1, 2, 3). The default value of n is 3.

-seed seed
Specify the seed of the random number generator used during simulation. The default value of seed is 1.

-rate
Trigger the CTMC simulation and computation of throughputs.

Note: This option is currently superfluous (if it is absent from the command-line, a warning message is issued but the functioning of cunctator is unchanged), its current purpose being to anticipate possible future extensions of the tool.

-save context_file
Save the context reached at the end of the current simulation in a binary file context_file, which can be reused by a future invocation of cunctator with the -restore option in order to start another simulation exactly from the point at which the current simulation terminated. Not a default option.

The context stored in context_file upon termination of the current simulation includes the following information: the state of the CTMC, the number of transitions of the sequence traversed during simulation, the simulation time, and the state of the random number generator (which will be used to restart the random number generator in the future invocations of cunctator with -restore that reuse the context stored in context_file). The format of context_file is undocumented and subject to future changes.

-restore context_file
Restore the context stored in context_file by a previous invocation of cunctator with the -save option and start a new simulation from that context. Not a default option.

If option -depth is present on the command-line, the current simulation will terminate according to the depth indicated by this option. The number of new transitions explored during the current simulation is equal to the difference between depth and the number of transitions d of the sequence restored from context_file. In other words, the current simulation will terminate when the total number of transitions traversed during this simulation and during the previous simulation whose termination context was stored in context_file becomes equal to depth. If depth <= d, then the current simulation terminates immediately and a warning message is issued. Option -time is handled similarly.

If the option -action is present on the command-line, it is ignored in favor of the corresponding actions restored from context_file.

If the options -seed or -scheduler are present on the command-line, they have higher precedence than the corresponding values restored from context_file. This makes possible two kinds of simulation scenarios:

- One can perform a first simulation sim1, save its context C, and start one or several simulations from C, but with seed and scheduler parameters different than those of sim1. This is useful, e.g., when the sim1 simulation is intended to go over some initial "transient" behaviour of the system, after which several simulations, with different seed and scheduler parameters, can be performed in order to study the "steady" behaviour of the system.

- If one must ensure that the former simulation whose termination context is stored in context_file is a proper prefix of the current simulation, then the options -seed and -scheduler must be absent from the command-line. In this way, a simulation sim1 terminating in context C followed by a simulation sim2 starting from C yields the same results as a single simulation sim having the same seed and scheduler as sim1 and having the same termination conditions (depth or time) as sim2.

If the options -hide or -rename were present on the command-line of the previous invocation of cunctator which produced context_file, they must also be present (with exactly the same arguments) on the command-line of the current invocation of cunctator in order to ensure that the former simulation is a proper prefix of the current simulation.

Note: When the options -save and -restore are simultaneously present on the command-line, they can use the same file context_file. This file will be first read in order to restore the context from which the current simulation is started, then rewritten upon termination of the simulation in order to save the context reached at that point.

-verbose
Animate the user's screen, telling what is going on. Not a default option.

-version
Display the current version number of the tool and stop. To be effective, this option should occur as the first argument on the command line. Subsequent options and/or arguments, if any, will be discarded. Not a default option.

Exit Status

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

Diagnostics

When the transition labels of the CTMC spec do not have the right format, error messages are issued.

Authors

The tool was developed and documented by Radu Mateescu (INRIA/VASY), with the advice of Holger Hermanns (INRIA/VASY). It is derived from the generator tool of CADP, developed by Hubert Garavel (INRIA/VASY). Meriem Zidouni (Bull and INRIA/VASY) suggested various improvements (such as the computation of throughputs for several actions) concerning the prototype version 0.5 of the tool.

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
sequence file (input)

See Also

bcg , bcg_open , caesar , caesar.adt , caesar.open , caesar_graph , caesar_hide_1 , caesar_rename_1 , exp.open , fsp.open , lnt.open , seq.open , regexp

A related CTMC simulator for studying biological models was developed by Verena Wolf (Saarland University).

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 Radu.Mateescu@inria.fr


Table of Contents