The Modest Toolset
Contact us
Documentation
Examples
Publications
Download
(This documentation of the modes tool is a work in progress. It will slowly be extended over time.)
The modes tool is a statistical model checker, i.e. a Monte Carlo simulator for formal models and properties. It is able to exploit multi-core CPUs and can run in a distributed manner across heterogeneous networked systems. It includes rare event simulation methods, and supports lightweight scheduler sampling (LSS) for nondeterministic models. For the science behind modes, we refer the interested reader to the current tool paper.
To list all command-line options supported by modes, run modest modes -?. The basic usage is to invoke modes on a model file, say model.modest:
modest modes model.modest
This performs statistical model checking of the model and all properties specified in model.modest. Supported input formats are Modest and JANI. modes automatically determines the input format based on the file extension; in case this fails, the input format can explicitly be specified via the -I parameter as -I Modest or -I JANI. Some models are parametrised, i.e. they contain constants for which no value is specified. For these models, multiple sets of parameter values can be specified for modes to independently analyse:
modest modes model.txt -E "N=16, MAX=2" -E "N=32, MAX=4"
To analyse models from the quantitative verification benchmark set without having to manually download the model files, use qcomp:// URLs, e.g.
modest modes qcomp://brp -E "N=16, MAX=2"
to download and analyse the bounded retransmission protocol model for parameter values N=16 and MAX=2. To analyse only a subset of the properties specified in a model, use the --props parameter:
modest modes qcomp://brp -E "N=16, MAX=2" --props "p1, p2"
By default, modes prints the analysis results to console. To additionally write the results to file results.txt in JSON format, run
modest modes model.modest -O results.txt Json
Alternative output formats are Text, which uses the same formatting as the output printed to console, and Minimal to write one line per property result plus the overall runtime only. To overwrite the output file without asking for confirmation, add the -Y parameter.
The --no-var-opt parameter disables all optimisations that change the set of model variables, which is useful when collecting traces. The --flatten parameter unrolls all parallel composition in the model prior to compilation instead of independently executing and synchronising the parallel components on-the-fly at simulation time. For most models, --flatten will reduce performance and increase memory usage. To disable certain run-time checks (such as bounded integer and array bounds checks and assignment consistency checks) for improved simulation performance, add the --unsafe parameter. This may result in invalid models being analysed, and should consequently not be used except on trusted and validated models.
modes contains dedicated simulation engines for different model types. By default, it attempts to automatically determine the a model's type and the corresponding best simulation engine. However, in some cases, the auto-detection may choose a more general engine than necessary; and for some model types, multiple engines are available. In such cases, the model type and engine can be specified manually:
modest modes model.modest -M RepresentativePTA
instructs modes to treat the model as a probabilistic timed automaton (PTA) and use its region representatives-based engine. The following model types and simulation engines are available:
The more expressive a model type is, the more involved is the simulation process. For optimal performance, therefore, the most restrictive engine that is applicable to the model at hand should be chosen. For PTA, we recommend the RegionPTA engine. A PTA can alternatively be converted into its digital clocks MDP for simulation with the MDP engine by specifying the --digital-clocks parameter.
(Documentation on modes' statistical evaluation methods will be added here.)
(Documentation on how to collect simulation traces will be added here.)
The core of statistical model checking, Monte Carlo simulation, is easy to parallelise. modes supports distributing the simulation effort over CPU cores in multiple threads, and over multiple networked machines.
By default, modes uses the local machine only, with as many simulation threads as the machine has logical cores minus one. At least one additional thread will concurrently aggregate and evaluate the simulation results. To specify a different number of simulation threads, use the -J parameters, e.g.
modest modes model.modest -J 4
to use four simulation threads.
(Documentation on how to use modes in a distributed fashion across networked machines will be added here.)
Modest uses pseudo-random number generators (PRNGs) to perform Monte Carlo simulation. The default PRNG used during simulation is the Mersenne Twister 19937 (MT19937) generator. Other generators can be requested; for example,
modest modes model.modest --rng XorShift
makes modes use a multiply-with-carry XOR-shift generator. The following generators are currently available:
By default, modes initialises its PRNGs with a different seed on every invocation. Therefore, it may produce different results on every invocation, subject to the statistical guarantees provided by its statistical evaluation methods. In particular, these guarantees are typically statements about multiple random invocations, so the use of a different seed per invocation is crucial for the validity of these guarantees. In some situations, however, precise repeatability is desired, e.g. when creating artifacts to be independently evaluated and archived. For these purposes, modes can be configured to produce the same result on every invocation by specifying a fixed seed:
modest modes model.modest -J 1 --seed 289348078
The above command also disables multi-threading by setting -J 1 since the unpredictable scheduling of multiple threads by the operating system would otherwise uncontrollable randomness. For the same reason, distributed simulation cannot be used to achieve repeatable results, either. When using lightweight scheduler sampling, the seed for scheduler sampling must also be fixed to obtain repeatable results using the --schedulers-seed parameter.
Rare event simulation is implemented in modes via the importance splitting technique, with support for automatically determining or manually specifying all ingredients of the procedure: the splitting method, the importance function, and the splitting levels. It can be used to analyse probabilistic reachability properties that query for the probability of reaching a set of goal states G without first entering a set of avoid states A. In Modest, these properties are specified as
property Prop = Pmax(!A U G);
with Boolean expressions for A and G. As the probabilities to be estimated in rare event simulation are usually unknown but small, we recommend to use the --relative-width parameter.
modes provides the RESTART and fixed effort splitting methods, including a weighted variant of fixed effort. They are enabled and configured via the --rare parameter. The RESTART method has a single numerical parameter determining the prolongation depth; it is 0 by default. To perform fully automated rare event simulation with RESTART with prolongation depth 1:
modest modes qcomp://brp -E "N=16,MAX=2" --props p2 --relative-width --rare Restart 1
To use fixed effort or its weighted variant instead, replace Restart by FixedEffort or WeightedFixedEffort and remove the prolongation depth parameter:
modest modes qcomp://brp -E "N=16,MAX=2" --props p2 --relative-width --rare WeightedFixedEffort
All methods are configurable in terms of the "effort" they spend per splitting level via the --rare-effort parameter. For RESTART, this is the splitting factor (which is 2 by default, and is ignored when levels are manually specified or the level calculation method is expected success). For FixedEffort, the effort is the number of runs per level (by default 64). For WeightedFixedEffort, it is the base number of runs per level (by default 32), which is multiplied by the splitting factor. For example,
modest modes qcomp://brp -E "N=16,MAX=2" --props p2 --relative-width --rare FixedEffort --rare-effort 1000
performs rare event simulation to estimate the value of property p2 of the bounded retransmission protocol model using the fixed effort splitting method with a very high effort of 1000 per-level runs.
The importance function in importance sampling is supposed to provide an indication of how "far" a state is from a state in G. It is ideally zero for all initial states, and takes its maximum value for all states in G.
By default, modes attempts to automatically derive an importance function in a compositional manner. In a simplified summary, this works as follows: First, modes exhaustively explores each parallel component's local state space. In this step, it overapproximates the set of reachable local states where global variables and synchronisation are involved, which may lead to unreachable and thus invalid states being explored, and may result in very large local state spaces in certain models. It then transforms the expression characterising G into an expression g in negation normal form and computes the graph distance of each local state to the set of local states that satisfy some of the literals of this expression. Given a state, the resulting compositional importance function then returns the sum of these distances as computed on the corresponding local states for each literal along the expression tree of g. Instead of using the distance, modes can be instructed to alternatively use the probability of reaching a local goal by specifying --ifun-calc Probability. These values are rounded as specified by the --ifun-precision parameter. The operations used to combine the local values along the expression tree of g, i.e. over conjunctions and disjunctions, can be changed from the default of Add for addition by specifying Max (maximum), Min (minimum), or Mul (multiplication) for the --ifun-op parameter, where the first value applies to disjunctions and the second value applies to conjunctions:
modest modes qcomp://brp -E "N=16,MAX=2" --props p2 --relative-width --rare Restart --ifun-op Max Min
The automated compositional importance function derivation does not work for every model, and it does not always find the best importance function. For such cases, modes can alternatively use an ad-hoc importance function specified via the --ifun-prop parameter. This parameter takes the name of a property included in the model, which must be a numeric state formula. modes then takes the property's value in each state as the state's importance. It can automatically determine the importance of the initial state. To determine the importance of the goal states, modes by default searches for such states; once it finds one, its importance is assumed to be the importance of the goal set. Finding such a state may take a long time; we therefore recommend to specify the goal set importance as part of the --ifun-prop parameter. For example,
modest modes model.modest --relative-width --rare Restart --ifun-prop Importance 0 12
instructs modes to use the property named Importance specified in model.modest as the importance function, assume that its value for all initial states is 0, and that its value for goal states is 12.
Importance splitting works by splitting a simulation run into multiple "child runs" once it jumps to a state of higher importance. However, it is typically not useful to split every time the importance increases; instead, we would like to do so only on specific thresholds where it is most beneficial, and split into an appropriate number of child runs. The thresholds determine ranges of importance values called splitting levels, and the number of child runs to split into is a level's splitting factor. By default, modes tries to automatically determine the levels and splitting factors using the expected success method with a target of one success per run on average. This is equivalent to running modes with the --levels ExpectedSuccess 1 parameter. Alternative splitting methods are
Of these, only ExpectedSuccess and Manual provide not only levels but also splitting factors; if they are used, then RESTART ignores the value specified for --rare-effort. In contrast, the fixed effort method always uses the fixed splitting factor specified for --rare-effort, ignoring any factors computed by expected success or specified manually. With StaticNumber and StaticWidth, the weighted fixed effort method is the same as the fixed effort method. As an example,
modest modes qcomp://brp -E "N=16,MAX=2" --props p2 --relative-width --rare Restart --levels StaticWidth 10
uses RESTART with a splitting factor of 2 (its default when --rare-effort is not specified) for each of the levels of width 10.
(Documentation on how to use modes' lightweight scheduler sampling feature will be added here.)
(Documentation on how to use rare event simulation in modes will be added here.)