|
| 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] cunctator [cunctator_opt] [parameter=value ...]
or:
fsp.open [fsp_opt] spec[.lts] [cc_opt] cunctator [cunctator_opt] [parameter=value ...]
or:
lnt.open [lnt_opt] spec[.lnt] [cc_opt] cunctator [cunctator_opt] [parameter=value ...]
or:
lotos.open [lotos_opt] spec[.lotos] [cc_opt] cunctator [cunctator_opt] [parameter=value ...]
or:
seq.open [seq_opt] spec[.seq] [cc_opt] cunctator [cunctator_opt] [parameter=value ...]
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:
rate %f" (called a stochastic transition),
; rate %f" (called a labelled stochastic transition), or
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.
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 optional list of "parameter=value" arguments at the end of the command line (where parameter is any character string that neither contains blanks nor the "=" character, and where value is any character string that does not contain blanks) is only meaningful to option -thr. The various "parameter" strings must be pairwise distinct. These arguments have no influence on the actual numerical computations, they only serve to add columns in throughput tables (see section OUTPUT-2 in the bcg_steady manual page).
The following options cunctator_opt are currently available:
; 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.
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.
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.
If both options -action and -thr are present on the command-line, the option -action is ignored in favor of -thr.
If both options -depth and -time are present on the command-line, the option -depth is ignored in favor of -time.
- 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.
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.
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.
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.
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.