Skip to content

v2.0.0

Latest
Latest

Choose a tag to compare

View all tags
@volkm volkm released this 21 Oct 12:29
· 4 commits to master since this release
2.0.0
44567cd
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.
  • Version 2.0 is a major release with numerous breaking changes to the API, command-line options and behaviour.
  • Model checking results now carry upper and lower bounds that can be queried via the API and are included in the command-line output, and sound solution bounds are available for DTMC/MDP model checking methods.
  • Improved model checking of interval MDPs (iMDPs and interval DTMCs): added expected time (Tmin/max=? [F "target"]) and cumulative rewards (Rmin/max=? [C<=k]), and Rmin=? [F "target"] on models without zero-reward end components. Fixed the computation of Rmin/max=? [F "target"].
  • Added a native CVC5 SMT solver backend. The SMT solver is selected in the environment; places without an environment use a solver chosen at compile time.
  • Revised and significantly sped up sparse bisimulation.
  • Added merging of equivalent states as a preprocessing step.
  • Added support for the WeakUntil (W) and Release (R) operators in properties: they are now accepted when parsing JANI, and Storm's formula handling supports them.
  • Faster model building.
  • Added model tolerance: sparse models now store the tolerance used to decide whether a model is valid, for example whether transition probabilities sum to one. It is set from the model builder or a command-line flag, and bisimulation uses it by default. It is independent of the precision used in verification.
  • --precision is now interpreted as the distance between the bounds and the value (half-width) in interval iteration and the topological solver. GVI uses relative precision if it is set.
  • Added support for certificate computation for reachability probabilities and expected rewards on MDPs
  • storm-pomdp:
    • Revised belief exploration: modular belief storage, exploration and abstraction, with unfolding, discretization and grid clipping, independently selectable numeric types, and reward-bounded reachability.
    • Added extraction and export of POMDP policies as finite-state controllers from belief unfolding (--export-policy, JSON or DOT).
    • Added a high-level API for belief-based verification of reachability probabilities and rewards.
  • storm-pars:
    • Added sequential convex programming (SCP) as a new method for parameter feasibility synthesis (storm-pars --feasibility).
    • Revised the storm-pars API, including verify and checkFeasibility functions for simple parameter synthesis, and moved graph conditions to storm-pars/analysis.
    • Refactored the monotonicity module.
    • Added a region constraint checker.
  • storm-counterexamples:
    • Counterexamples now support JANI models with multiple locations.
  • Bug fixes:
    • Incorrect exit rates in DD-based Markov automaton bisimulation quotients.
    • Early termination of iterative (min-max) linear equation solvers with custom termination conditions, which terminated only if both bounds satisfied the condition.
    • Hybrid engine with sound computations.
    • DTMC model checking of conditional probabilities now throws an error if the condition is unreachable.
    • Interval model checking now sets results only for maybe states.
    • JANI parsing of boolean operators over path formulae.
    • DRN parser now throws an error if the order of rewards and labels is wrong.
    • fitsIntoStoredType rejecting negative int64_t encodings.
    • FragmentChecker discarding recursive results.
    • Multi-objective properties and feature restriction.
    • POMDP analysis now rejects unsupported threshold formulae.
    • mtbdd_iszero on non-leaf nodes in sylvan.
    • LTO (link-time optimization) was only applied at the link step and thus ineffective since version 1.11.0; it is now applied at compile time as well.
  • Dependencies:
    • Updated Spot to version 2.16, googletest to 1.18.0 and carl-storm to 14.37.
    • Eigen is now fetched from its GitHub mirror; 3rd-party dependencies are declared via FetchContent_Declare.
  • Developer:
    • Moved files from src/storm/storage to more fitting locations such as storm/languages, storm/expressions/ and storm/dd/. See doc/files_moved.md for the full list of file and namespace changes.
    • Added SubmatrixBuilder; SparseMatrixBuilder now has an accumulation mode and is stricter about dimensions in build(..).
    • Added ExtendedNumber to replace infinities on rationals.
    • Added ccache support to the Dockerfiles. Revised CI.
Assets 6
Loading