The Modest Toolset Contact us Documentation Examples Publications Download


Build 3.1. 42 (2020-05-26): Added the --es parameter to perform essential states reduction in mcsta.
Build 3.1. 41 (2020-05-19): Added support for long-run average value simulation in modes.
Build 3.1. 39 (2020-03-22): Added support for interruptible sampling in lightweight scheduler sampling in modes.
Build 3.1. 37 (2020-03-20): Added the --no-partial-results parameter to disable returning partial results in mcsta.
Build 3.1. 25 (2019-12-11): Added support for smart sampling in lightweight scheduler sampling in modes.
Build 3.1. 13 (2019-11-05): Added support for checking expected-reward properties with interval iteration in mcsta.
Build 3.1. 12 (2019-09-23): Added optimistic value iteration as a solution method in mcsta.
Build 3.1. 11 (2019-09-21): Added sound value iteration as a solution method in mcsta.
Build 3.1. 10 (2019-09-19): Added the mobench tool to automate benchmarking.
Build 3.1.  2 (2019-06-16): Added support for qcomp:// URLs, e.g. "qcomp://beb", to load models from the quantitative verification benchmark set in all tools.
Build 3.1.  0 (2019-06-03): The Modest Toolset now uses the .NET Core runtime; all tools have been consolidated into the modest command.

Build 3.0.136 (2019-04-17): Added support for long-run average properties in mcsta.
Build 3.0.132 (2019-03-25): Added the IMCA format for state space exporting in mcsta.
Build 3.0.129 (2019-03-19): Added linear programming as a solution method in mcsta.
Build 3.0.128 (2019-03-17): Added the --exhaustive parameter to explore the complete state space, including irrelevant states, in mcsta.
Build 3.0.122 (2019-03-10): Added the --statespace parameter to export the explored state space to file in mcsta.
Build 3.0.121 (2019-03-09): Added the switch-step algorithm for time-bounded reachability in MA in mcsta.
Build 3.0.111 (2019-02-17): Added the --location-vars parameter to detect and expand location variables in moconv.
Build 3.0.110 (2019-02-04): Added the mopy tool to export Python code for state space exploration.
Build 3.0.108 (2019-01-13): Changed the default value of the --rng parameter to MersenneTwister in modes.
Build 3.0.106 (2018-12-18): Changed the scheduler output to include only states reachable with that scheduler for unbounded properties in mcsta.
Build 3.0.104 (2018-12-09): Added the new adaptive sampling method by Chen and Xu in modes.
Build 3.0.101 (2018-12-01): Added interval iteration as an alternative to value iteration in mcsta.
Build 3.0.100 (2018-11-29): Fixed incorrect conversion of exit rewards to branch rewards in mcsta, moconv, modes, and mosta.
Build 3.0. 99 (2018-11-28): Added the --props parameter to select the properties to analyse in mcsta, moconv, modes, mosta, and prohver.
Build 3.0. 98 (2018-11-27): Added support for sampling from discretised continuous distributions, e.g. "i = floor(min(LogNormal(0, 0.5), 3.68))", in mcsta.
Build 3.0. 97 (2018-11-21): Added "option" declarations to request special semantics for DTMC, CTMC, and CTMDP in Modest.
Build 3.0. 90 (2018-10-15): Added support for checking properties with nontrivial until formulas in mcsta.
Build 3.0. 89 (2018-10-14): Added the --partial parameter to use model checking based on partial exploration in mcsta.
Build 3.0. 88 (2018-10-09): Added the --ec parameter to perform end component reduction in mcsta.
Build 3.0. 86 (2018-08-30): Added support for time-bounded properties on Markov automata in mcsta.
Build 3.0. 85 (2018-08-28): Improved the JSON-based results format to report per-property timings in mcsta.
Build 3.0. 84 (2018-08-27): Added the "with" construct to specify location transient values, "constrain" as a synonym for "invariant", and support for state exit rewards with accumulation symbol "X" in Modest.
Build 3.0. 80 (2018-08-16): Added support for properties that compare a probability or expected value to a constant expression in mcsta.
Build 3.0. 78 (2018-08-09): Improved the handling and reporting of floating-point inaccuracies in mcsta.
Build 3.0. 77 (2018-08-08): Improved trace output to more precisely state the reson for the end of the trace in modes.
Build 3.0. 72 (2018-07-29): Added the --precision parameter to specify the precision of probabilities exported to PHAVER in prohver.
Build 3.0. 71 (2018-07-26): Fixed crashes with certain patterns of process calls in Modest.
Build 3.0. 68 (2018-07-19): Added support for finite-range nondeterministic assignments in mcsta, modes, and prohver.
Build 3.0. 65 (2018-07-08): Fixed incorrect handling of synchronisation with PTA and STA models in mcsta, and of incorrect computation of rewards with Markov automata models in modes.
Build 3.0. 64 (2018-06-28): Added support for writing results to file in a JSON-based format in mcsta, modes, and prohver.
Build 3.0. 62 (2018-06-21): Added parameters to specify the initial and target values of ad-hoc importance functions in modes.
Build 3.0. 61 (2018-06-19): Added syntax for indexed assignments "{= 1: i = 1, 2: i++ =}" in Modest.
Build 3.0. 60 (2018-06-18): Added support for branch reward-bounded and expected rate reward properties on Markov automata in mcsta.
Build 3.0. 59 (2018-06-16): Added support for model checking of unbounded properties on Markov automata in mcsta.
Build 3.0. 47 (2018-05-22): Added the ability to export models with open parameters in moconv.
Build 3.0. 42 (2018-05-01): Added the --collect-schedulers option to obtain a histogram of per-scheduler results in modes.
Build 3.0. 33 (2018-03-22): Fixed the evaluation of properties during zone-based simulation in modes.
Build 3.0. 31 (2018-03-21): Fixed the handling of user-specified seeds for random number generation in modes.
Build 3.0. 28 (2018-03-07): Changed the formatting of location variables to use location names in traces printed by modes and in schedulers printed by mcsta.
Build 3.0. 23 (2018-01-19): Added the --thread-budget parameter to enable throttling of unbalanced simulation threads in modes.
Build 3.0. 22 (2018-01-04): Improved the performance of lightweight scheduler sampling in modes.
Build 3.0. 20 (2017-11-19): Fixed excessive syntactic checks that rejected valid SHA models in prohver.
Build 3.0. 19 (2017-11-14): Fixed crash when chain compression is enabled and the model does not use any rewards in mcsta.
Build 3.0. 18 (2017-11-03): Added a bash script that automates the distributed execution of modes on Slurm-based clusters, and the --scheduler-levels parameter to recalculate splitting levels for every scheduler in modes.
Build 3.0. 16 (2017-10-30): Added the --independent parameter to use independent simulation runs for all properties in modes.
Build 3.0. 11 (2017-10-25): Improved the state space generation and simulation performance for models with many components and synchronising transitions, and removed the --buffer-size parameter in modes.
Build 3.0.  9 (2017-10-18): Added support for two-phase scheduler sampling in modes.
Build 3.0.  8 (2017-10-14): Improved parallelism across properties and schedulers in modes.
Build 3.0.  7 (2017-10-03): Added support for distributed rare-event simulation in modes.
Build 3.0.  6 (2017-10-02): Added support for rectangular hybrid automata in modes.