Many Tools Support the UMB Format
Storm (version 1.12) integrates UMB support (either compressed or uncompressed) for import and export of Markov automata, stochastic games, POMDPs and all their special cases, including interval- or rational-valued transitions and including rich annotations on states and observations. The support is deeply embedded and thus Storm provides an interface also to, e.g., fault trees or Petri nets, or can be used to provide, e.g., bisimulation quotients of models.
Visit Site
In the Modest toolset, the mcsta probabilistic model checker has been rebuilt around the UMB format.
Its internal data structures match the files and binary representation of UMB, allowing mcsta to load UMB files by simply mapping them into memory via mmap.
It supports reading UMB files encoding LTSs, DTMCs, CTMCs, MDPs, and MAs, and can generate files for such models
given in JANI or the Modest language.
As working with unchecked pointers/array indexing on untrusted UMB data could easily create security vulnerabilities, mcsta includes a strict UMB validator that thoroughly checks the metadata and binary files for semantic consistency and data ranges.
PRISM, as of version 4.10, provides UMB import and export for all models supported by both the tool and the format, notably Markov chains, MDP and POMDPs, interval variants of all these, and LTSs.
This includes rewards, atomic propositions, valuations for states/observations
and either floating point or exact arithmetic models.
PRISM-games, as of version 3.2.2, provides the same functionality for turn-based stochastic games.
Support for reading and writing UMB files has been implemented as a standalone Java library umbj.
.umb files.
Similarly, PET, which uses Prism's input parser, will support UMB through Prism's umbj library.