To support the creation of Modest models, and to compute the values of properties or check requirements specified as part of models, the Modest Toolset [1]} provides a collection of visualisation, model transformation, model checking, and simulation tools.
The Modest Toolset has been in development since 2008; it is written in C#, and is available as precompiled binaries for common Linux distributions, macOS, and Windows at modestchecker.net.
As input languages, it supports Modest and JANI; its moconv tool can convert between the two and apply various transformations, such as converting a suitable PTA model into its digital clocks [2]} MDP.
The mosta tool visualises a model's symbolic semantics, helping in learning Modest and in debugging models.
The mopy tool converts a model into Python code implementing a first-state-next-state interface [3]} that can be used to quickly prototype explicit-state verification algorithms and that is used by the author as part of the programming project of a Master's-level course on quantitative verification at the University of Twente.
