Changelog
Development:
------------
- Modest: Added support for mutually recursive user-defined functions.
- Modest: Added support for recursive datatypes (formerly called structs).
- Modest: Added support for option types.
- Modest: Added support for constant expressions as array lengths.
- Modest: Added shorter aliases for the continuous probability distributions: "Exp", "Uni" and "Norm".
- Modest: Added new "var" and "reward" types to explicitly mark continuous and reward variables.
- Modest: Added the "any" operator for nondeterministic assignments, e.g. "x = any(y | y > 4)".
- Modest: Added support for arrays of clocks, rewards and continuous variables.
- Modest: Added broadcast synchronisation (similar to UPPAAL) (declare as "broadcast action a;", use as "a!" or "a?").
- Modest: Changed the invariant construct from a shorthand to a first-class Modest construct.
- Modest: Changed bracing ({}) requirements for try-catch, relabel and other constructs to be more consistent.
- Modest: Changed the syntax for dealing with derivatives (use invariants instead of assignments). See [HHHK12] for details.
- Modest: Removed support for explicit guarded parallel composition. Use sequential composition instead.
- Modest: Removed support for "did" and "can" in properties.
- mcpta: Added support for transition rewards.
- mcpta: Added check for PRISM version. Only PRISM version 4 is supported.
- mosta: Added the mosta tool to visualise the NSTA semantics of Modest models using Graphviz dot.
Version 1.3.4:
--------------
- Modest: Added binary synchronisation (as in CCS) (declare as "binary action a;", use as "a!" or "a?").
- Modest: Added construct "restrict B P" to force synchronisation with binary actions.
- Modest: Changed syntax for fixed-size arrays: They must now specify a size, as in "int[3] arr;"
- Modest: Changed syntax for bounded integer types: "int i limit [N..M]" is now "int(N..M) i".
- Modest: Removed support for implicitly-typed user-defined functions.
- mcpta: Fixed property translation to support PRISM 4.0.
- mctau: Added the mctau tool for model-checking and visualisation of networks of timed automata with UPPAAL 4.1.4 and later.
Version 1.3.3:
--------------
- Bugfix release.
Version 1.3.2:
--------------
- modes: Added static optimization of expressions and unused variables/functions/processes.
- modes: Added support for selective output of traces based on a condition over properties.
- modes: Added support for terminating simulation runs upon decision of all properties.
- modes: Added "Stochastic" scheduler for randomized choice of delay.
- mcpta: Disabled support for diagonal clock constraints temporarily (was broken in previous versions).
Version 1.3.1:
--------------
- Modest: Added shorthand "when urgent(e) P" for "when(e) urgent(e) P".
- Modest: Added shorthand "delay(e, c) P" for "D()" where "process D(){ clock d; real x = e; when urgent(d >= x && c) P }"
- Modest: Changed syntax for patient/impatient action declarations: "patient"/"impatient" now occurs before "action".
- mime: Fixed handling of real-valued parameters in experiments.
- mcpta: Fixed handling of arrays for multiply nested processes.
- mcpta: Improved handling of clock variables that are never compared to any other value or variable.
- modes: Added interactive simulation.
- modes: Improved performance, notably for partial order reduction code.
- modes: Fixed various bugs, notably a missing bounds check in the ALAP scheduler.
Version 1.3:
------------
- Modest: Added support for new probability distributions: Binomial, Poisson, Geometric, Normal
- Modest: Added shorthands in assignments: ++ and --
- Modest: Changed syntax and semantics for property specification.
- Modest: Changed the semantics of the palt construct (no more no_weight and neg_weight exceptions).
- mime: Added configuration options for font and tab settings.
- mime: Added the possibility to zoom in and out of the whole user interface.
- mime: Added persistence of UI layout.
- mime: Added commands to export Modest code to HTML, LaTeX and XPS.
- mime: Added support for drag & drop to open files in mime.
- mime: Changed scope of persisted analysis engine configurations: they are now saved per engine and (open) model.
- mcpta: Added option to choose the PRISM engine used.
- mcpta: Added option to control the use of the -fixdl parameter for PRISM.
- modes: Improved simulation performance (speed and memory) significantly.
- mcpta: Fixed bugs that prevented diagonal clock constraints from working correctly.
- modes: Changed the algorithm for partial order based detection of nondeterminism to a correct one.
