The Modest Toolset Contact us Documentation Examples Publications Download


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 in Modest.
                            Added "constrain" as a synonym for "invariant" in Modest.
                            Added 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.
                            Fixed 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.
                            Added 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.
                            Improved the status and progress display during scheduler sampling 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.
                            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.