You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

140 lines
6.8 KiB

8 years ago
8 years ago
8 years ago
8 years ago
  1. Changelog
  2. ==============
  3. This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog.
  4. The releases of major and minor versions contain an overview of changes since the last major/minor update.
  5. Version 1.3.x
  6. -------------
  7. ### Version 1.3.1 (under development)
  8. - Added support for multi-dimensional quantile queries
  9. - Allow to quickly check a benchmark from the [Quantitative Verification Benchmark Set](http://qcomp.org/benchmarks/) using the --qvbs option.
  10. - Added script resources/examples/download_qvbs.sh to download the QVBS.
  11. - If an option is unknown, Storm now prints a hint to similar option names.
  12. - JANI: Allow bounded types for constants
  13. - JANI: Support for non-trivial reward accumulations.
  14. - JANI: Fixed support for reward expressions over non-transient variables.
  15. - Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial)
  16. - Fixed linking with Mathsat on macOS
  17. - Fixed compilation for macOS mojave
  18. ### Version 1.3.0 (2018/12)
  19. - Slightly improved scheduler extraction
  20. - Environments are now part of the c++ API
  21. - Heavily extended JANI support, in particular:
  22. * arrays, functions, state-exit-rewards (all engines)
  23. * indexed assignments, complex reward expressions (sparse engine)
  24. * several jani-related bug fixes
  25. - New binary `storm-conv` that handles conversions between model files
  26. - New binary `storm-pomdp` that handles the translation of POMDPs to pMCs.
  27. - Maximal progress assumption is now applied while building Markov Automata (sparse engine).
  28. - Improved Unif+ implementation for Markov Automata, significantly reduced memory consumption.
  29. - Added support for expected time properties for discrete time models
  30. - Bug fix in the parser for DRN (MDPs and MAs might have been affected).
  31. - `storm-gspn`: Improved .pnpro parser
  32. - `storm-gspn`: Added support for single/infinite/k-server semantics for GSPNs given in the .pnpro format
  33. - `storm-gspn`: Added option to set a global capacity for all places
  34. - `storm-gspn`: Added option to include a set of standard properties when converting GSPNs to jani
  35. - `storm-pars`: Added possibility to compute the extremal value within a given region using parameter lifting
  36. - `storm-dft`: DFT translation to GSPN supports Don't Care propagation
  37. - `storm-dft`: Support DFT analysis via transformation from DFT to GSPN to JANI
  38. - `storm-dft`: Added SMT encoding for DFTs
  39. - `storm-dft`: Improved Galileo and JSON parser
  40. - Several bug fixes
  41. - Storm uses the `master14` branch of carl from now on
  42. ### Comparison with Version 1.2.0 (details see below)
  43. - Heavily extended JANI-support
  44. - New binary `storm-conv` that handles conversion between model files
  45. - New binary `storm-pomdp` that handles the translation of POMDPs to pMCs.
  46. - `storm-gspn` improved
  47. - Sound value iteration
  48. Version 1.2.x
  49. -------------
  50. ### Version 1.2.3 (2018/07)
  51. - Fix in version parsing
  52. ### Version 1.2.2 (2018/07)
  53. - Sound value iteration (SVI) for DTMCs and MDPs
  54. - Topological solver for linear equation systems and MinMax equation systems (enabled by default)
  55. - Added support for expected total rewards in the sparse engine
  56. - By default, iteration-based solvers are no longer aborted after a given number of steps.
  57. - Improved export for jani models
  58. - A fix in parsing jani properties
  59. - Several extensions to high-level counterexamples
  60. - `storm-parsers` extracted to reduce linking time
  61. - `storm-counterexamples` extracted to reduce linking time
  62. - `storm-dft`: improvements in Galileo parser
  63. - `storm-dft`: test cases for DFT analysis
  64. - Improved Storm installation
  65. - Several bug fixes
  66. ### Version 1.2.1 (2018/02)
  67. - Multi-dimensional reward bounded reachability properties for DTMCs.
  68. - `storm-dft`: transformation of DFTs to GSPNs
  69. - Several bug fixes
  70. ### Version 1.2.0 (2017/12)
  71. - C++ api changes: Building model takes `BuilderOptions` instead of extended list of Booleans, does not depend on settings anymore.
  72. - `storm-cli-utilities` now contains cli related stuff, instead of `storm-lib`
  73. - Symbolic (MT/BDD) bisimulation
  74. - Fixed issue related to variable names that can not be used in Exprtk.
  75. - DRN parser improved
  76. - LP-based MDP model checking
  77. - Sound (interval) value iteration
  78. - Support for Multi-objective multi-dimensional reward bounded reachability properties for MDPs.
  79. - RationalSearch method to solve equation systems exactly
  80. - WalkerChae method for solving linear equation systems with guaranteed convergence
  81. - Performance improvements for sparse model building
  82. - Performance improvements for conditional properties on MDPs
  83. - Automatically convert MA without probabilistic states into CTMC
  84. - Fixed implemention of Fox and Glynn' algorithm
  85. - `storm-pars`: support for welldefinedness constraints in mdps.
  86. - `storm-dft`: split DFT settings into IO settings and fault tree settings
  87. - `storm-dft`: removed obsolete explicit model builder for DFTs
  88. - Features for developers:
  89. * Solvers can now expose requirements
  90. * unbounded reachability and reachability rewards now correctly respect solver requirements
  91. * Environment variables (such as the solver precisions) can now be handled more flexible
  92. * changes to Matrix-Vector operation interfaces, in particular fixed some issues with the use Intel TBB
  93. Version 1.1.x
  94. -------------
  95. ### Version 1.1.0 (2017/8)
  96. - Support for long-run average rewards on MDPs and Markov automata using a value-iteration based approach.
  97. - Storm can now check MDPs and Markov Automata (i.e. MinMax equation systems) via Linear Programming.
  98. - Parametric model checking is now handled in a separated library/executable called `storm-pars`.
  99. - Wellformedness constraints on PMCs:
  100. * include constraints from rewards
  101. * are in smtlib2
  102. * fixed
  103. * computation of only constraints without doing model checking is now supported
  104. - Fix for nested formulae
  105. - JANI: Explicit engine supports custom model compositions.
  106. - Support for parsing/building models given in the explicit input format of IMCA.
  107. - Storm now overwrites files if asked to write files to a specific location.
  108. - Changes in build process to accommodate for changes in carl. Also, more robust against issues with carl.
  109. - `USE_POPCNT` removed in favor of `FORCE_POPCNT`. The popcnt instruction is used if available due to `march=native`, unless portable is set.
  110. Then, using `FORCE_POPCNT` enables the use of the SSE 4.2 instruction
  111. Version 1.0.x
  112. -------------
  113. ### Version 1.0.1 (2017/4)
  114. - Multi-objective model checking support now fully included
  115. - Several improvements in parameter lifting
  116. - Several improvements in JANI parsing
  117. - Properties can contain model variables
  118. - Support for rational numbers/functions in decision diagrams via sylvan
  119. - Elimination-based solvers (exact solution) for models stored as decision diagrams
  120. - Export of version and configuration to cmake
  121. - Improved building process
  122. ### Version 1.0.0 (2017/3)
  123. Start of this changelog