Moves Rwth Storm Versions Save

• Added support for multi-dimensional quantile queries.
• Added support for multi-objective model checking under pure (deterministic) schedulers with bounded memory using --purescheds.
• Allow to quickly check a benchmark from the Quantitative Verification Benchmark Set using the --qvbs option.
• Added script resources/examples/download_qvbs.sh to download the QVBS.
• If an option is unknown, Storm now suggests similar option names.
• Flagged several options as 'advanced' to clean up the --help-message. Use --help all to display a complete list of options.
• Support for parsing of exact time bounds for properties, e.g., P=? [F=27 "goal"].
• Export of optimal schedulers when checking MDPs with the sparse engine (experimental). Use --exportscheduler <filename>.
• PRISM language: Support for the new round operator.
• PRISM language: Improved error messages of the parser.
• JANI: Allow bounded types for constants.
• JANI: Support for non-trivial reward accumulations.
• JANI: Fixed support for reward expressions over non-transient variables.
• DRN: Added support for exact parsing and action-based rewards.
• DRN: Support for placeholder variables which allows to parse recurring rational functions only once.
• Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial).
• Support for export of MTBDDs from Storm.
• Support for k-shortest path counterexamples (arguments -cex --cextype shortestpath)
• New settings module transformation for Markov chain transformations. Use --help transformation to get a list of available transformations.
• Support for eliminating chains of Non-Markovian states in MAs via --eliminate-chains.
• Export to dot format allows for maximal line width in states (argument --dot-maxwidth <width>)
• storm-conv can now apply transformations on a prism file.
• storm-pars: Enabled building, bisimulation and analysis of symbolic models.
• storm-dft: Support partial-order for state space generation.
• storm-dft: Compute lower and upper bounds for number of BE failures via SMT.
• storm-dft: Allow to set relevant events which are not set to Don't Care.
• storm-dft: Support for constant failed BEs. Use flag --uniquefailedbe to create a unique constant failed BE.
• storm-dft: Support for probabilistic BEs via PDEPs.
• Fixed linking with Mathsat on macOS.
• Fixed linking with IntelTBB for GCC.
• Fixed compilation for macOS Mojave and higher.
• Several bug fixes.

• Slightly improved scheduler extraction
• Environments are now part of the c++ API
• Heavily extended JANI support, in particular:
  • arrays, functions, state-exit-rewards (all engines)
  • indexed assignments, complex reward expressions (sparse engine)
  • several jani-related bug fixes
• New binary storm-conv that handles conversions between model files
• New binary storm-pomdp that handles the translation of POMDPs to pMCs.
• Maximal progress assumption is now applied while building Markov Automata (sparse engine).
• Improved Unif+ implementation for Markov Automata, significantly reduced memory consumption.
• Added support for expected time properties for discrete time models
• Bug fix in the parser for DRN (MDPs and MAs might have been affected).
• storm-gspn: Improved .pnpro parser
• storm-gspn: Added support for single/infinite/k-server semantics for GSPNs given in the .pnpro format
• storm-gspn: Added option to set a global capacity for all places
• storm-gspn: Added option to include a set of standard properties when converting GSPNs to jani
• storm-pars: Added possibility to compute the extremal value within a given region using parameter lifting
• storm-dft: DFT translation to GSPN supports Don't Care propagation
• storm-dft: Support DFT analysis via transformation from DFT to GSPN to JANI
• storm-dft: Added SMT encoding for DFTs
• storm-dft: Improved Galileo and JSON parser
• Several bug fixes
• Storm uses the master14 branch of carl from now on

Comparison with Version 1.2.0

• Heavily extended JANI-support
• New binary storm-conv that handles conversion between model files
• New binary storm-pomdp that handles the translation of POMDPs to pMCs.
• storm-gspn improved
• Sound value iteration

• Fix in version parsing

• Sound value iteration (SVI) for DTMCs and MDPs
• Topological solver for linear equation systems and MinMax equation systems (enabled by default)
• Added support for expected total rewards in the sparse engine
• By default, iteration-based solvers are no longer aborted after a given number of steps.
• Improved export for jani models
• A fix in parsing jani properties
• Several extensions to high-level counterexamples
• storm-parsers extracted to reduce linking time
• storm-counterexamples extracted to reduce linking time
• storm-dft: improvements in Galileo parser
• storm-dft: test cases for DFT analysis
• Improved Storm installation
• Several bug fixes

This release is an update from 1.2.1 to support archiving of our TACAS submission. We are aware of an issue under GCC 7 with LTO enabled.

• Multi-dimensional reward bounded reachability properties for DTMCs.
• storm-dft: transformation of DFTs to GSPNs
• Several bug fixes

• C++ api changes: Building model takes BuilderOptions instead of extended list of Booleans, does not depend on settings anymore.
• storm-cli-utilities now contains cli related stuff, instead of storm-lib
• Symbolic (MT/BDD) bisimulation
• Fixed issue related to variable names that can not be used in Exprtk.
• DRN parser improved
• LP-based MDP model checking
• Sound (interval) value iteration
• Support for Multi-objective multi-dimensional reward bounded reachability properties for MDPs.
• RationalSearch method to solve equation systems exactly
• WalkerChae method for solving linear equation systems with guaranteed convergence
• Performance improvements for sparse model building
• Performance improvements for conditional properties on MDPs
• Automatically convert MA without probabilistic states into CTMC
• Fixed implemention of Fox and Glynn' algorithm
• storm-pars: support for welldefinedness constraints in mdps.
• storm-dft: split DFT settings into IO settings and fault tree settings
• storm-dft: removed obsolete explicit model builder for DFTs
• Features for developers:
  • Solvers can now expose requirements
  • unbounded reachability and reachability rewards now correctly respect solver requirements
  • Environment variables (such as the solver precisions) can now be handled more flexible
  • changes to Matrix-Vector operation interfaces, in particular fixed some issues with the use Intel TBB

• Support for long-run average rewards on MDPs and Markov automata using a value-iteration based approach.
• Storm can now check MDPs and Markov Automata (i.e. MinMax equation systems) via Linear Programming.
• Parametric model checking is now handled in a separated library/executable called storm-pars.
• Wellformedness constraints on PMCs:
  • include constraints from rewards
  • are in smtlib2
  • fixed
  • computation of only constraints without doing model checking is now supported
• Fix for nested formulae.
• JANI: Explicit engine supports custom model compositions.
• Support for parsing/building models given in the explicit input format of IMCA.
• Storm now overwrites files if asked to write files to a specific location.
• Changes in build process to accommodate for changes in carl. Also, more robust against issues with carl.
• USE_POPCNT removed in favor of FORCE_POPCNT. The popcnt instruction is used if available due to march=native, unless portable is set. Then, using FORCE_POPCNT enables the use of the SSE 4.2 instruction.

First stable release of Storm.

Several additions that did not make it into the v1.0.0 release:

• Multi-objective model checking support now fully included
• Several improvements in parameter lifting
• Several improvements in JANI parsing
• Properties can contain model variables
• Support for rational numbers/functions in decision diagrams via sylvan
• Elimination-based solvers (exact solution) for models stored as decision diagrams
• Export of version and configuration to cmake
• Improved building process