v1.8.1

Workaround for issue with Boost >= 1.81

v1.8.0

• Revised implementation of value iteration algorithms and its variants, fixing a bug in the optimistic value iteration heuristic.
• Experimental support for compiling on Apple Silicon.
• Added SoPlex as a possible LP solver.
• Upgraded shipped version of sylvan.
• Upgraded repo / version for carl (for polynomials), requires carl-storm in at least version 14.23.
• Removed support for just-in-time compilation (JIT). If the JIT engine is needed, use Storm version 1.7.0.
• storm-dft: better modularization: improved algorithm for finding independent modules and revised the DFT analysis via modularization.
• storm-dft: added checks whether a given DFT is well-formed and conventional.
• storm-pomdp: streamlined implementation for quantitative analysis.
• storm-pomdp: added clipping for POMDP under-approximation.
• storm-pomdp: added API for interactive exploration of belief MDPs.
• Developer: Introduced forward declarations (in their own headers), in particular for storm::RationalNumber, storm::RationalFunction, and storm::json.
• Developer: LpSolver interface now supports RawMode (to avoid overhead of storm::expression) and indicator constraints.

v1.7.0

• Fixed a bug in LP-based MDP model checking.
• DRN Parser is now more robust, e.g., it does no longer depend on tabs.
• PRISM Parser: Modulo with negative numbers is now consistent with Prism.
• Added lexicographic multi-objective model checking. Use --lex in the command line interface when specifying a multi(...) property.
• Fix handling duplicate entries in the sparse matrix builder.
• Added support for step-bounded until formulas in LTL.
• Added Dockerfile.
• API: Applying a fully defined deterministic memoryless scheduler to an MDP yields a DTMC.
• storm-dft: Use dedicated namespace storm::dft.
• storm-dft: Added support (parsing, export, BDD analysis) for additional BE failure distributions (Erlang, log-normal, Weibull, constant probability).
• storm-dft: Added instantiator for parametric DFT.
• Developer: Storm is now built in C++17 mode.
• Developer: Added support for automatic code formatting for storm-dft.

v1.6.4

• Added support for model checking LTL properties in the sparse (and dd-to-sparse) engine. Requires building with Spot or an external LTL to deterministic automaton converter (using option --ltl2datool).
• Added cmake options STORM_USE_SPOT_SYSTEM and STORM_USE_SPOT_SHIPPED to facilitate building Storm with Spot.
• Improved parsing of formulas in PRISM-style syntax.
• Added export of schedulers that use memory (in particular optimizing schedulers for LTL properties)
• Added support for PRISM models that use unbounded integer variables.
• Added support for nested arrays in JANI.
• Added --location-elimination that can be applied to Jani DTMC models to reduce the size of the resulting Markov models, see here.
• Added an export of check results to json. Use --exportresult in the command line interface.
• Added --exportbuilt option that exports the built model in various formats. Deprecates --io:exportexplicit, --io:exportdd and --io:exportdot
• Added export of built model in .json. which can be used to debug and explore the model.
• Added computation of steady state probabilities for DTMC/CTMC in the sparse engine. Use --steadystate in the command line interface.
• Added computation of the expected number of times each state in a DTMC/CTMC is visited (sparse engine). Use --expvisittimes in the command line interface.
• Implemented parsing and model building of Stochastic multiplayer games (SMGs) in the PRISM language. No model checking implemented (yet).
• API: Simulation of prism-models
• API: Model-builder takes a callback function to prevent extension of particular actions, prism-to-explicit mapping can be exported
• API: Export of dice-formatted expressions
• Prism-language/explicit builder: Allow action names in commands writing to global variables if these (clearly) do not conflict with assignments of synchronizing commands.
• Prism-language: n-ary predicates are supported (e.g., ExactlyOneOf)
• Added support for continuous integration with Github Actions.
• storm-pars: Exploit monotonicity for computing extremal values and parameter space partitioning.
• storm-dft: Support for analysis of static fault trees via BDDs (Flag --bdd). In particular, efficient computation of multiple time bounds was added and support for several importance measures (Argument --importance).
• storm-dft: Computation of minimal cut sets for static fault trees (Flag --mcs).
• storm-dft: Improved modularisation for DFT by exploiting SFT analysis via BDDs.
• storm-dft: Fixed don't care propagation for shared SPAREs which resulted in wrong results.
• Developer: Added support for automatic code formatting and corresponding CI workflow.

v1.6.3

• Added support for multi-objective model checking of long-run average objectives including mixtures with other kinds of objectives.
• Added support for generating optimal schedulers for globally formulae
• Simulator supports exact arithmetic
• Added switch --no-simplify to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs)
• Fixed issues with JANI inputs concerning
  • transient variable expressions in properties,
  • constants in properties, and
  • integer variables with either only an upper or only a lower bound.
• storm-pomdp: States can be labelled with values for observable predicates
• storm-pomdp: (Only API) Track state estimates
• storm-pomdp: (Only API) Reduce computation of state estimates to computation on unrolled MDP

v1.6.2

• Prism program simplification improved.
• Revamped implementation of long-run-average algorithms, including scheduler export for LRA properties on Markov automata.
• Support for step-bounded properties of the form ... [F[x,y] ... ] for DTMCs and MDPs (sparse engine).
• Renamed portfolio engine to automatic
• storm-dft: Fix for relevant events when using symmetry reduction.
• storm-pomdp: Fix for --transformsimple and --transformbinary when used with until formulae.
• storm-pomdp: POMDPs can be parametric as well.

v1.6.0

• Changed default Dd library from cudd to sylvan. The Dd library can be changed back to cudd using the command line switch --ddlib.
• Scheduler export: Properly handle models with end components. Added export in .json format.
• CMake: Search for Gurobi prefers new versions
• CMake: We no longer ship xerces-c. If xerces-c is not found on the system, storm-gspn will not be able to parse xml-based GSPN formats
• CMake: Added option STORM_LOAD_QVBS to automatically download the quantitative verification benchmark set.
• Eigen library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode versions.
• Tests: Enabled tests for permissive schedulers
• storm-counterexamples: fix when computing multiple counterexamples in debug mode
• storm-dft: Renamed setting --show-dft-stats to dft-statistics and added approximation information to statistics.
• storm-pomdp: Implemented approximation algorithms that explore (a discritization of) the belief MDP, allowing to compute safe lower- and upper bounds for a given property.
• storm-pomdp: Implemented almost-sure reachability computations: graph-based, one-shot SAT-based, and iterative SAT-based
• storm-pomdp: Various changes such that transformation to pMCs is now again supported (and improved)
• Fixed several compiler warnings.

v1.5.1

• Jani models are now parsed using exact arithmetic.

v1.5.0

• Added portfolio engine which picks a good engine (among other settings) based on features of the symbolic input.
• Abort of Storm (via timeout or CTRL+C for example) is now gracefully handled. After an abort signal the program waits some seconds to output the result computed so far and terminates afterwards. A second signal immediately terminates the program.
• Setting --engine dd-to-sparse --bisimulation now triggers extracting the sparse bisimulation quotient.
• JIT model building is now invoked via --engine jit (instead of --jit).
• DRN: support import of choice labelling.
• Added option --build:buildchoiceorig to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. --exportscheduler).
• Implemented optimistic value iteration for sound computations and set it as new default in --sound mode.
• Time bounded properties for Markov automata are now computed with relative precision. Use --absolute for the previous behavior.
• Apply the maximum progress assumption while building a Markov automaton with one of the symbolic engines.
• Added option --build:nomaxprog to disable applying the maximum progress assumption during model building (for Markov Automata).
• Added hybrid engine for Markov Automata.
• Improved performance of the Unif+ algorithm (used for time-bounded properties on Markov Automata).
• Various performance improvements for model building with the sparse engine.
• storm-dft: Symmetry reduction is now enabled by default and can be disabled via --nosymmetryreduction.
• storm-pomdp: Only accept POMDPs that are canonical.
• storm-pomdp: Prism language extended with observable expressions.
• storm-pomdp: Various fixes that prevented usage.
• Several bug fixes.

v1.4.1

• Implemented long run average (LRA) computation for DTMCs/CTMCs via value iteration and via gain/bias equations.
• Added several LRA related settings in a new settings module. Note that --minmax:lramethod has been replaced by --lra:nondetmethod.