@volkm volkm released this Aug 10, 2017 · 1611 commits to master since this release

Assets 2
  • 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.