While Modest is a convenient modelling language for end-users, the work required to implement code that parses Modest models and transforms the parsed syntax into its symbolic semantics (a parallel composition of SHA with discrete variables) is nontrivial.
The same problem affects many other modelling languages, e.g. Prism's [1]}, too.
To ease tool development and facilitate the exchange of models between different tools, in 2016, the developers of several quantitative verification tools defined the JSON-based JANI [2]} format.
It is not designed to be human-writable, but rather serve as a model interchange format that is generated by tools from other modelling languages, such as Modest.
Today, JANI is supported by the Modest Toolset (see below), Storm [3]}, Momba [4]}, and several other tools.
All models in the quantitative verification benchmark set (QVBS) [5]} are available in both their original formats as well as in JANI.
The QVBS served as the foundation for the QComp 2019 [6]} and QComp 2020 [7]} tool competitions.
