A Modern Probabilistic Model Checker
Workaround for issue with Boost >= 1.81
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.storm::RationalNumber
, storm::RationalFunction
, and storm::json
.storm::expression
) and indicator constraints.--lex
in the command line interface when specifying a multi(...)
property.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.storm-dft
.--ltl2datool
).STORM_USE_SPOT_SYSTEM
and STORM_USE_SPOT_SHIPPED
to facilitate building Storm with Spot.--location-elimination
that can be applied to Jani DTMC models to reduce the size of the resulting Markov models, see here.--exportresult
in the command line interface.--exportbuilt
option that exports the built model in various formats. Deprecates --io:exportexplicit
, --io:exportdd
and --io:exportdot
--steadystate
in the command line interface.--expvisittimes
in the command line interface.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.--no-simplify
to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs)storm-pomdp
: States can be labelled with values for observable predicatesstorm-pomdp
: (Only API) Track state estimatesstorm-pomdp
: (Only API) Reduce computation of state estimates to computation on unrolled MDPstorm-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.cudd
to sylvan
. The Dd library can be changed back to cudd
using the command line switch --ddlib
..json
format.STORM_LOAD_QVBS
to automatically download the quantitative verification benchmark set.storm-counterexamples
: fix when computing multiple counterexamples in debug modestorm-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-basedstorm-pomdp
: Various changes such that transformation to pMCs is now again supported (and improved)--engine dd-to-sparse --bisimulation
now triggers extracting the sparse bisimulation quotient.--engine jit
(instead of --jit
).--build:buildchoiceorig
to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. --exportscheduler
).--sound
mode.--absolute
for the previous behavior.--build:nomaxprog
to disable applying the maximum progress assumption during model building (for Markov Automata).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.