v1.14.0

• Moved from settings to environments or options in several places:
  • LP solvers
  • Model building
  • Bisimulation
  • Parsing
  • Symbolic models
• Revised state and observation valuations.
• Added support for HiGHS MILP solver.
• Renamed --additional-checks to --check-zeno.
• Removed deprecated --lex argument. Lexicographic model checking can be invoked using the multilex(..) syntax.
• Reintroduced sample-derivative for storm-pars.
• Bug fixes:
  • Parsing of Prism files such as observables and reserved keywords.
  • Parsing of constant strings and negative number in commandline options.
  • Parsing of DRN files with rational intervals.
  • Multi-objective model checking for negative rewards.
  • WeightVectorChecker for negative weights.
  • In Valuations.
  • Setting relative precision in LRA.
  • Scheduler extraction for topological solver.
  • State elimination for absorbing states.
  • Synchronization vector for non-synchronizing JANI choices.
  • MDP model checking of globally properties via hybrid engine.
  • Memory products and initial states.
• Requires CMake >= 3.25.
• Updated gmm version to 5.5.
• Moved from parallel-hashmap to gtl.
• Developer: Sped up compilation of storm-parsers and storm-pars.
• Developer: Sped up tests by skipping a few costly tests.
• Developer: Fixed a number of compiler warnings.
• Developer: Cleaned up parts of code base such as state elimination and cli-utilities.
• Developer: Added support for clang-tidy.
• Developer: Improved code quality via reports from clang-tidy.
• Developer: Consistent handling of includes, asserts and throwing of exceptions.
• Developer: Introduced STORM_LOG_STATS.
• Developer: Added CMake option STORM_COMPILE_WITH_PCH.
• Developer: Added Copilot instructions.

v1.13.0

• Moved repository to stormchecker/storm.
• Import/export of explicit models in (binary) UMB format.
• Support for exact intervals, parsing exact intervals from Prism and bounded model checking of interval DTMC and interval MDP.
• Support for monitor verification.
• Extended support for conditional model checking.
• Added scheduler to ExplicitQualitativeCheckResult.
• Adaption to changes of CMake options in carl-storm.
• Revised installation paths.
• Updated dependencies: carl-storm, ExprTk, Spot.
• Renamed directories: storm-cudd and cpphoafparser.
• Bug fixes:
  • in Unif+ for Markov automata with non-Markovian initial states
  • dangling reference to tmp object
  • assert in observation trace unfolder
  • warning in ConditionalHelper
  • error for IDTMC checking from CLI
  • in includes
  • compiler warnings
• Developer: Added support for intervals in multipliers.
• Developer: Extended differentation of ValueType and SolutionType in more places.
• Developer: Added support for creating Debian packages in CMake and via CI workflow.
• Developer: minor fixes in CI workflows.

v1.12.0

• Support for verifying IDTMCs.
• Extended DRN file format:
  • Use --io:digits option to control precision of floats.
  • Reading from and writing to compressed DRN files (use .drn.gz / .drn.xz file extensions and/or the new --compression option) (requires libarchive).
  • Added @value_type to determine the type of the parsed values.
  • Support for parsing of DRN interval models.
• Multi-objective model checking:
  • Multi-objective model checking in --soundmode handles approximation errors correctly.
  • Added --multiobjective:approxtradeoff setting to control Pareto curve approximation heuristic.
  • Extended support for multi-objective properties: distinguish between trade-off and lexicographic properties, introduce multilex(..) syntax for Prism-style properties.
• storm-pars:
  • Added BigStep transformation.
  • Added generalized parameter lifting.
  • Support for not graph-preserving regions and for not well-defined regions.
  • Region verification API uses RefinementOptions.
• Support build without DD support.
• Added state-valuation transformer.
• Preparation for using probability matrix in CTMC bisimulation.
• Revised check for probabilistic transition matrix.
• ConstantsComparator no longer depends on global state.
• New (optional) dependency: libarchive which supports directly reading/writing from an archive.
• Updated dependencies: carl-storm, Eigen, ExprTk, gmm, googletest, Gurobi, parallel-hashmap, Spot.
• Bug fixes in returning rate parameters and requiring MultiObjectiveSettings.
• Developer: modernized CTMC helpers.
• Developer: general code clean up such as revising includes, assertions and CMake defines.
• Developer: CI treats compiler warnings as errors.

v1.11.1

• Bug fixes in conditional probabilities computation with the (recent) bisection method.
• Sound value iteration diagnostics in debug mode are more robust.
• Improved support for ARM.
• Support for musl libc.
• Code quality fixes (reduced warnings)

v1.11.0

• Completely restructured CMake build process:
  • Storm can now be properly installed.
  • Carl-storm is now automatically fetched from a predefined repository and tag. Use CMake option -DFETCHCONTENT_SOURCE_DIR_CARL=<path_to_carl> to set a local path.
• Improved support for interval models, especially parsing support for Prism models with intervals and CLI support for interval models.
• Support for discounted properties in DTMCs and MDPs.
• Added guessing value iteration.
• Support exporting schedulers for multi-objective properties.
• Revised implementation of conditional probabilities for MDPs.
• Added building of choice labels for Jani.
• Support time limits for the Gurobi LP Solver.
• Various fixes in DRN parser, BitVector, (negative) expected rewards, parsing of PDEP and for compiler warnings.
• Updated dependencies: carl-storm, gmm, googletest, l3pp, spot.
• Removed support for Intel TBB.
• Developer: Replaced GmmxxMultiplier by ViOperatorMultiplier.
• Developer: Added CI workflow for new releases.

v1.10.0

• Improved LpMinMaxLinearEquationSolver, set relevant values in topological solvers.
• Speed up of MEC decomposition by adjusting loops.
• Minor improvements for steady-state properties.
• Improved access to state valuations.
• Improved parsing: detect and handle integer overflows in expression parsing, and handle irrational probability expressions.
• Limit Sylvan threads to 1 on Apple Silicon.
• Bug fixes in computation of cumulative rewards, transient variables in JANI, SMGs with non-synchronizing but labeled actions, in SparseCbAchievabilityQuery and PcaaWeightVectorChecker.
• Updated shipped dependencies: Eigen, ExprTk, Spot.
• storm-dft: Set BDD variable ordering for SFT from file.
• storm-dft: Warning on potential modeling issues.
• storm-dft: Bug fixes in DFT representant computation and failable elements.
• storm-pars: Bug fixes in monotonicity computation.
• storm-pomdp: Added cut-off memory node information.
• storm-pomdp: Extended handling of terminal states.
• storm-pomdp: Improved output.
• Developer: Require at least CMake version 3.22.
• Developer: Revised includes.
• Developer: GLPK is optional.
• Developer: BitVector conforms to std::ranges::range concept.
• Developer: Improved CI tests and added builds on macOS.

v1.9.0

• Improved expected visiting times (EVTs) and steady state distribution computations.
• Support for interval-based models.
• Robust VI.
• Significantly improved compilation times.
• Support for logarithm expressions in PRISM and JANI.
• Support for sin and cos operators, and PI and Euler constants in JANI parser.
• Extraction of schedulers for minimal expected total rewards.
• More efficient MEC and SCC decompositions.
• Revised LP encoding for multi-objective verification under simple strategies.
• Added CLI option --permute to re-order the states after building.
• Added CLI option --build:state limit <number> to limit the number of explored states.
• Print all linked libraries when using --version.
• Removed support for HyPro and Cuda.
• Moved gamebased-ar to own library.
• Various bug fixes.
• storm-conv: Removed option --stdout.
• storm-dft: Fixes and improvements for DFT symmetries and DFT simulation.
• storm-pars: Completely reworked the command-line interface (and partially the C++ API).
• storm-pars: "Time travelling" optimization.
• storm-pgcl: Removed the library.
• Developer: Require at least CMake version 3.15.
• Developer: Moved storm-config.h.in into src directory.
• Developer: Use various Dockerfiles in CI.
• Developer: Revised includes and use pre-compiled headers.
• Developer: Fixed various compiler warnings.

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.