Skip to content

Releases: moves-rwth/storm

v1.9.0

22 Aug 12:52
5d5ebe4
Compare
Choose a tag to compare
  • 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

15 Jun 18:05
3f74f3e
Compare
Choose a tag to compare

Workaround for issue with Boost >= 1.81

v1.8.0

31 May 19:39
fd1fe70
Compare
Choose a tag to compare
  • 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

29 Jul 18:27
Compare
Choose a tag to compare
  • 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

13 Jan 11:23
4ec3f6a
Compare
Choose a tag to compare
  • 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

24 Nov 11:54
Compare
Choose a tag to compare
  • 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

04 Sep 12:59
Compare
Choose a tag to compare
  • 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

08 Jun 14:46
Compare
Choose a tag to compare
  • 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

16 Mar 14:16
Compare
Choose a tag to compare
  • Jani models are now parsed using exact arithmetic.

v1.5.0

12 Mar 15:22
Compare
Choose a tag to compare
  • 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.

DOI