- Added support for multi-dimensional quantile queries.
- Added support for multi-objective model checking under pure (deterministic) schedulers with bounded memory using
- Allow to quickly check a benchmark from the Quantitative Verification Benchmark Set using the
- Added script
resources/examples/download_qvbs.shto download the QVBS.
- If an option is unknown, Storm now suggests similar option names.
- Flagged several options as 'advanced' to clean up the
--help allto display a complete list of options.
- Support for parsing of exact time bounds for properties, e.g.,
P=? [F=27 "goal"].
- Export of optimal schedulers when checking MDPs with the sparse engine (experimental). Use
- PRISM language: Support for the new
- PRISM language: Improved error messages of the parser.
- JANI: Allow bounded types for constants.
- JANI: Support for non-trivial reward accumulations.
- JANI: Fixed support for reward expressions over non-transient variables.
- DRN: Added support for exact parsing and action-based rewards.
- DRN: Support for placeholder variables which allows to parse recurring rational functions only once.
- Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial).
- Support for export of MTBDDs from Storm.
- Support for k-shortest path counterexamples (arguments
-cex --cextype shortestpath)
- New settings module
transformationfor Markov chain transformations. Use
--help transformationto get a list of available transformations.
- Support for eliminating chains of Non-Markovian states in MAs via
- Export to dot format allows for maximal line width in states (argument
storm-convcan now apply transformations on a prism file.
storm-pars: Enabled building, bisimulation and analysis of symbolic models.
storm-dft: Support partial-order for state space generation.
storm-dft: Compute lower and upper bounds for number of BE failures via SMT.
storm-dft: Allow to set relevant events which are not set to Don't Care.
storm-dft: Support for constant failed BEs. Use flag
--uniquefailedbeto create a unique constant failed BE.
storm-dft: Support for probabilistic BEs via PDEPs.
- Fixed linking with Mathsat on macOS.
- Fixed linking with IntelTBB for GCC.
- Fixed compilation for macOS Mojave and higher.
- Several bug fixes.