Modest Toolset
Home Downloads Publications Case Studies Documentation Contact Us More Tools

modes User Manual

Table of Contents

  1. Introduction
  2. Valid Modest Fragment
    1. Deviations From Semantics
  3. Output Evaluation
    1. Termination of Simulation Runs
    2. Termination of Experiments
    3. Confidence Interval Estimation
    4. External Evaluation
  4. Random Number Generation
  5. Nondeterminism
    1. Schedulers
    2. Resolvers
    3. Partial Order Reduction
  6. Model Debugging Features
    1. Guard and Constraint Display Format
    2. Traces
    3. Trace Filters
    4. Conditional Traces
  7. Files and Directories Used By modes

  Introduction

modes [mʊˈdɛs] is a discrete event simulator for the Modest compositional modelling language, aiming to provide a reference implementation for Modest semantics. This document details the features of the modes discrete event simulator.

Detailed documentation of the command line interface can be found here. The graphical user interface is not documented at the time of this writing, but is believed to be sufficiently self-explanatory once one has studied the command line interface and this manual. Note that not all features exposed by the command line interface are currently available in the graphical user interface; such features are marked accordingly below.

  Valid Modest Fragment

Not all models that can be expressed in the Modest language are suitable for discrete event simulation with modes. To be simulated, models must fulfill the following requirements:

  Deviations From Semantics

  Output Evaluation

modes currently supports only output evaluation of independent replications. Properties of interest may be specified using the Unified Property Language (UPL) shared by all tools in the Modest toolset. Refer to the UPL documentation for details about syntax and the fragment implemented for modes.

Note that for all query-type properties except for the actual value query (Vmin/Vmax), the queries for the minimum and maximum values, respectively, will always return the same values in simulation. This is because these queries refer to the minimum and maximum values with respect to nondeterministic choices in the model. Since simulation can only be used to evaluate deterministic models (or nondeterministic models that have been made deterministic by imposing a scheduler), these values will always coincide.

  Termination of Simulation Runs

By default, modes will stop each simulation run as soon as all model properties have been decided, i.e. if it is certain that no future model behaviour, whatever it may be, can possibly change the values that have been observed thus far. Note that in general, there is no guarantee that this will ever happen; in particular, for some types of properties such as invariants (A[] STATE_PREDICATE), simulation can only decide with certainty that an invariant is violated, but not that it is fulfilled.

In cases where invariant properties or similar properties are of interest, the model should be constructed in such a way that simulation runs are finite by way of eventually ending in a deadlock or timelock. This way, the simulator can make a well-founded statement about the period observed up to the deadlock/timelock. Though even then, keep in mind that if the model is probabilistic, sections which are only probabilistically reachable may still have gone unobserved.

It is possible to set upper limits for the number of steps (-s/--steps) and amount of time (-t/--time) per simulation run, as well as a boolean termination predicate (-T/--stop-when) to avoid unintentionally non-terminating simulation runs. If these limits are met, simulation will be aborted with an error, as they are considered fail-safes to be used to ensure termination, not valid ways of terminating simulation runs.

If you understand the semantic implications and would prefer to simulate up to a specific point, use the --allow-limits option. The simulator will now terminate each run only when the maximum number of steps, the maximum amount of time or a state which fulfills the termination predicate is reached (and of course, if the model enters a deadlock before any of these conditions are met). The simulator will additionally ignore the state of model properties and continue simulating of to the given limits even if properties have already been decided.

Note

If a model does not have any properties at all, a warning will be issued and the simulator will behave as if the --allow-limits option had been specified.

  Termination of Experiments

There are two options available for specifying when two terminate an experiment. The first option is to specify some number of runs which will be executed; afterwards, the data gathered from these runs will be evaluated. The second, more versatile option is to specify a set of termination criteria. These will be evaluated continuously during simulation and the process will stop according to the state of these criteria. Note that these two modes are mutually exclusive.

To execute a number of runs which is fixed a-priori, use the -r/--runs option.

Termination criteria are given with the -U/--until option and adhere to the syntax described in the grammar below.

INT_CRIT    ::= ('samples' | 'minfail' | 'minsucc' | 'maxfail' | 'maxsucc') '(' <integer> ')'
REAL_CRIT   ::= ('ciwidth' | 'relciwidth') '(' <real> ')'
NP_CRIT     ::= 'nofail' | 'nosucc' | 'certain'
CRITERION   ::= INT_CRIT | REAL_CRIT | NP_CRIT
PROP_LIST   ::= PROPLIST <property>
CRIT_DECL   ::= CRITERION ':' PROP_LIST
            ::= CRITERION ':' '*'
CRITERIA    ::= CRIT_DECL
              | CRITERIA ';' CRIT_DECL

The atomic criteria are divided into necessary criteria and sufficient criteria. The experiment will terminate if either at least one sufficient criterion is fulfilled, or alternatively, if all necessary criteria have been fulfilled. Note that most criteria can only be applied to specific types of properties and will cause an error when applied to other types.

Note that although criteria can be specified with a list of properties, they will be evaluated individually for each of the specified properties, meaning that for a necessary criterion, it must be fulfilled for all listed properties, and for a sufficient criterion, it is enough for it to be fulfilled by just one of the listed properties.

Instead of a list of properties, an asterisk (*) may be used to automatically fill in all properties which support the preceding criterion.

Necessary criteria:

Sufficient criteria:

Instead of manually specifying criteria, the keyword default may be passed to the -U/--until option to fill in the following defaults:

  Confidence Interval Estimation

modes will automatically estimate a confidence interval for the mean value of all model properties (if applicable) when executing multiple runs, except when there was not enough data gathered to make a meaningful estimate. For expected value queries, the confidence interval assumes approximately normal-distributed data. For probabilistic reachability queries, the Agresti-Coull interval is used.

For expected value and probabilistic reachability hypotheses, modes will compute one-sided confidence limits using the same assumptions as for the interval computations mentioned above. If either the hypothesis or its negation can be accepted with the given level of confidence, modes will report a decision; otherwise, modes will report that the result is uncertain, but show the computed sample mean and sample standard deviation.

  External Evaluation

modes allows you to write the data gathered from individual runs to a file for manual inspection or for use with another tool. To do this, specify the desired output format and output file name using the --dump-format and --dump-results options. Currently, there are three output formats available: regular CSV data with headers, TAB-separated CSV with headers commented out (suitable for gnuplot) and XML.

The XML format is structured into a set of experiments, each of which contain the set of model parameters for that experiment (if any) and for each performed simulation run, a set of observed values for each property. The generated XML files contain inline DTD, describing the format.

  Random Number Generation

Modes allows the user to choose between three different pseudo-random number generation algorithms to use as a source for random numbers during simulation. These algorithms are described in the following paragraphs. A fourth 64 bit wide LCG-type algorithm is used internally for generating seeds.

When invoking modes from the command line, the random number generation algorithm is selected by specifying the --rn-generator option. In mime, the random number generator can be selected in the experiment settings. The default is Mersenne Twister.

Lagged Fibonacci

A lagged Fibonacci generator of the form xn = (xn-j + xn-k) mod 2N, width j=5, k=17 and N=32, yielding a period of 231(217-1). It is the fastest random number generator with the smallest memory footprint implemented by modes. However, lagged Fibonacci generators are sensitive to initialization and may behave suboptimally in some scenarios.

Mersenne Twister (MT19937)

The popular random number generator developed by Makoto Matsumoto and Takuji Nishimura with a period of 219937-1. The implementation used in modes includes the improved initialization as of 2002.

Complementary Multiply With Carry

A fast generator with good randomness, developed by George Marsaglia. The version implemented by modes has a period of about 1013101. It is faster than the Mersenne Twister, however, it also has a larger memory footprint.

  Nondeterminism

Models containing nondeterminism are not suitable for evaluation by discrete event simulation. However, sometimes it is desirable to make explicit assumptions to remove nondeterminism present in a model in some fashion. modes provides the user with a set of predefined schedulers to resolve nondeterminism.

Resolving nondeterminism in this way is not recommended, because only a subset of the specified behaviour can be observed this way, although the ASAP scheduler is useful to simulate untimed systems. However, in general it is not true that the ASAP/ALAP schedulers produce the shortest/longest possible paths through the system as reported by a model checker and using the schedulers in such a way may produce unexpected results.

A special case arises in a class of models whose Modest specification is nondeterministic, but which are weakly bisimilar to a deterministic specification, meaning that any conceivable resolution of the nondeterminism present in the original nondeterministic specification will lead to the same results. This happens frequently in models containing parallel composition, where the order of execution of non-synchronizing transitions is not uniquely defined because of the interleaving semantics used. Such "spurious" nondeterminism can be detected and ignored by modes, if desired; see the "Partial Order" resolver below.

modes differentiates between two kinds of nondeterminism (ND), namely temporal ND and structural ND. Temporal ND arises whenever the amount of time to wait in a certain state before taking the next transition is not uniquely defined by applicable guards and urgency constraints. Structural ND arises whenever there are multiple transitions enabled at the same time such that the next transition to be taken is not uniquely defined.

Below, you will find the details on the available strategies to resolve temporal ND (schedulers) and the strategies to resolve structural ND (resolvers).

Note

Temporal nondeterminism is always resolved before structural nondeterminism, i.e. the amount of time to remain in a state is chosen first, and then the next transition is picked from the set of transitions enabled at that point in time. Therefore, the choice of scheduler can have an effect on structural nondeterminism.

  Schedulers

  Resolvers

  Partial Order Reduction

Partial order reduction is a technique typically used to minimize a model's state space prior to analysis. This helps reduce the memory requirements of approaches which need to hold the entire state space (or significant portions of it) in memory at once. In simulation, the same basic methodology can be used to determine whether a set of transitions containing more than one element may be reduced to a singleton set without affecting observable output, thereby safely resolving the nondeterministic choice.

The approach implemented in modes involves a bounded look-ahead. You may need to manually adjust the look-ahead depth in order to successfully apply this approach to some models by using the -K/--partial-order-depth option (however, the default value of 8 was found to be sufficient for most models). modes will alert you to the possibility that the look-ahead depth may need to be increased whenever nondeterminism is reported as a result of not being able to make a decision prior to reaching the configured look-ahead depth.

For the partial order reduction approach to be correct, all loops in the model must contain at least one fully expanded (deterministic) state. Since loops cannot be distinguished from long sequences in the presence of variables with virtually infinite domain, the implementation uses a safe overapproximation which disallows long sequences without fully expanded states. The length of the longest permissible sequence is given by the -L/--partial-order-bound option. While the default of 128 should be sufficiently large for most practically interesting cases, it may be necessary to increase this value modes aborts simulation with a warning about a possible infinite loop of stutter steps.

Refer to our publication for more details about the algorithm.

  Model Debugging Features

modes offers debugging features designed to help better understand the behaviour of a model or to assist model design. Currently, these features are only available through the modes command line interface.

  Guard and Constraint Display Format

When presenting the user with a list of feasible events or events that contributed to an error condition such as unresolvable nondeterminism, the guards and urgency constraints for each event are shown. Guards and urgency constraints are shown as lists of time intervals in which the corresponding guard is enabled and the urgency constraint is urgent, respectively. There are several shorthands for particular kinds of interval lists, for example:

It is important to note that these time interval lists are always relative to the current point in time, so the guard { T=0 } is enabled "now", not exclusively at the beginning of the simulation run.

  Traces

When executing a single simulation run, modes will print a trace of the simulation run, showing which transitions where taken at which time, and which source code locations they originated from. This feature is automatically turned off by default when executing multiple runs, but it can be forced on if desired by using the -v/--verbosity option.

If you want to examine assignments in addition to the transitions taken, use the -v/--verbosity option to turn on debug traces. After each line, you will additionally see the assignments executed by the transition as well as the concrete values that were stored in the respective variables.

A fragment of a typical trace (without assignments) will look like this:

       Time              Transition Label      Source Location(s)

       2.190 :: [                     tau] :: [29:2]
                [                       a] :: [31:2  87:4  110:4]
                [                     tau] :: [113:128]
       2.419 :: [                       b] :: [34:4  92:2]
                [                       c] :: [33:2  109:4]
                [                     tau] :: [113:128]

Each line represents one transition in the automaton corresponding to the Modest model.

The first column has the value of the simulation clock. This column is omitted if the transition corresponding that line was instantaneous, i.e. did not take any time at all. In that case, the value remains the same as the last time it was shown, i.e. the first three lines of the trace fragment above all happened at time 2.19, and between the third and fourth line, there was a delay of 2.419–2.19=0.229 time units.

The second column contains the transition label. Note that this is the label in the composed automaton, meaning that it reflects active relabelings, hidings, etc.

The third and last column denotes the line and column in the original Modest source file of the action call (or other Modest construct) that generated this transition in the automaton. If multiple line/column pairs are given, this means that the transition was generated by a parallel composition of multiple component transitions. Each pair corresponds to one of the transitions that synchronized.

When using debug trace mode (trace with assignments), the assignments executed by each transition will be listed after the corresponding line in the regular trace.

When using the partial order resolver, observed steps are marked with a '=' sign (note that not all observable steps are necessarily observed; this information is computed from properties and the termination condition). Reduced steps, i.e. steps leaving states where a nondeterministic choice existed which was determined to be spurious, are marked with a capital 'R'.

  Trace Filters

Simulation traces can easily get long and crowded, when frequently one is only interested in a few specific variables, or a few specific transition labels (or conversely, one may wish to hide certain variables or labels that are known to be irrelevant). This can be achieved by using the -Q/--filter-labels and -F/--filter-updates options, both of which accept a simple filter expression which shows or hides transitions and variable updates based on the label or variable name.

Each filter consists of a comma-separated list of positive (no prefix) or negative (prefixed by !) wildcard expressions (*="anything", ?="any one", #="one or more digits") which are applied in order. The first expression in the list determines whether the filter as a whole is a positive filter (i.e. specifies elements which should pass) or a negative filter (i.e. specifies elements which should be rejected); the expressions which follow later in the sequence refine the filter successively.

Examples:

  Conditional Traces

Occasionally one wants to see only traces corresponding to runs which exhibit some rare feature or problem. To this end, modes allows the user to specify a conditional expression to filter out traces by the way in which they terminated (i.e. the state and value of model properties at termination as well as the reason for termination). The grammar follows the same syntax as regular Modest expressions, however these conditionals may not access model variables. They are constructed using the predicates and functions listed below.

The following predicates describing the termination mode of a simulation run may be used in the trace filter condition:

Additionally, the following predicates may be used to talk about properties:

  Files and Directories Used By modes

Output files which are directly requested by the user, such as dumps of raw result lists or traces, are saved to the current working directory. Other files, such as cached assemblies and accompanying files as well as dumps of generated code, are written to a common, system and configuration dependent location. On Windows-based systems, these files are stored in the local application data directory. On Mono, this directory is supplied by the XDG_DATA_HOME environment variable, or otherwise some system-dependent default.