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.

257 lines
15 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.6.x
  6. -------------
  7. ## Version 1.6.4 (20xx/xx)
  8. - Added support for model checking LTL properties in the sparse (and dd-to-sparse) engine. Requires building with Spot or an external LTL to deterministic automaton converter (using option `--ltl2datool`).
  9. - Added cmake options `STORM_USE_SPOT_SYSTEM` and `STORM_USE_SPOT_SHIPPED` to facilitate building Storm with [Spot](https://spot.lrde.epita.fr/).
  10. - Improved parsing of formulas in PRISM-style syntax.
  11. - Added export of schedulers that use memory (in particular optimizing schedulers for LTL properties)
  12. - Added support for PRISM models that use unbounded integer variables.
  13. - Added an export of check results to json. Use `--exportresult` in the command line interface.
  14. - Added computation of steady state probabilities for DTMC/CTMC in the sparse engine. Use `--steadystate` in the command line interface.
  15. - Implemented parsing and model building of Stochastic multiplayer games (SMGs) in the PRISM language. No model checking implemented (yet).
  16. - API: Simulation of prism-models
  17. - API: Model-builder takes a callback function to prevent extension of particular actions, prism-to-explicit mapping can be exported
  18. - API: Export of dice-formatted expressions
  19. - Prism-language/explicit builder: Allow action names in commands writing to global variables if these (clearly) do not conflict with assignments of synchronizing commads.
  20. - Prism-language: n-ary predicates are supported (e.g., ExactlyOneOf)
  21. - Added support for continuous integration with Github Actions.
  22. - `storm-pars`: Exploit monotonicity for computing extremal values and parameter space partitioning.
  23. ## Version 1.6.3 (2020/11)
  24. - Added support for multi-objective model checking of long-run average objectives including mixtures with other kinds of objectives.
  25. - Added support for generating optimal schedulers for globally formulae.
  26. - Simulator supports exact arithmetic.
  27. - Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs).
  28. - Fixed issues with JANI inputs concerning .
  29. - transient variable expressions in properties,
  30. - constants in properties, and
  31. - integer variables with either only an upper or only a lower bound.
  32. - `storm-pomdp`: States can be labelled with values for observable predicates.
  33. - `storm-pomdp`: (Only API) Track state estimates.
  34. - `storm-pomdp`: (Only API) Reduce computation of state estimates to computation on unrolled MDP.
  35. ## Version 1.6.2 (2020/09)
  36. - Prism program simplification improved.
  37. - Revamped implementation of long-run-average algorithms, including scheduler export for LRA properties on Markov automata.
  38. - Support for step-bounded properties of the form ... [F[x,y] ... ] for DTMCs and MDPs (sparse engine).
  39. - Renamed portfolio engine to automatic
  40. - `storm-dft`: Fix for relevant events when using symmetry reduction.
  41. - `storm-pomdp`: Fix for --transformsimple and --transformbinary when used with until formulae.
  42. - `storm-pomdp`: POMDPs can be parametric as well.
  43. ## Version 1.6.0 (2020/06)
  44. - Changed default Dd library from `cudd` to `sylvan`. The Dd library can be changed back to `cudd` using the command line switch `--ddlib`.
  45. - Scheduler export: Properly handle models with end components. Added export in `.json` format.
  46. - CMake: Search for Gurobi prefers new versions.
  47. - CMake: We no longer ship xerces-c. If xerces-c is not found on the system, storm-gspn will not be able to parse xml-based GSPN formats.
  48. - CMake: Added option `STORM_LOAD_QVBS` to automatically download the quantitative verification benchmark set.
  49. - Eigen library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode versions.
  50. - Tests: Enabled tests for permissive schedulers.
  51. - `storm-counterexamples`: fix when computing multiple counterexamples in debug mode.
  52. - `storm-dft`: Renamed setting `--show-dft-stats` to `dft-statistics` and added approximation information to statistics.
  53. - `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.
  54. - `storm-pomdp`: Implemented almost-sure reachability computations: graph-based, one-shot SAT-based, and iterative SAT-based.
  55. - `storm-pomdp': Various changes such that transformation to pMCs is now again supported (and improved).
  56. - Fixed several compiler warnings.
  57. Version 1.5.x
  58. -------------
  59. ## Version 1.5.1 (2020/03)
  60. - Jani models are now parsed using exact arithmetic.
  61. ## Version 1.5.0 (2020/03)
  62. - Added portfolio engine which picks a good engine (among other settings) based on features of the symbolic input.
  63. - Abort of Storm (via timeout or CTRL+C for example) is now gracefully handled. After an abort signal the program waits some seconds to output the result computed so far and terminates afterwards. A second signal immediately terminates the program.
  64. - Setting `--engine dd-to-sparse --bisimulation` now triggers extracting the sparse bisimulation quotient.
  65. - JIT model building is now invoked via `--engine jit` (instead of `--jit`).
  66. - DRN: support import of choice labelling.
  67. - Added option `--build:buildchoiceorig` to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. `--exportscheduler`).
  68. - Implemented optimistic value iteration for sound computations and set it as new default in `--sound` mode.
  69. - Time bounded properties for Markov automata are now computed with relative precision. Use `--absolute` for the previous behavior.
  70. - Apply the maximum progress assumption while building a Markov automaton with one of the symbolic engines.
  71. - Added option `--build:nomaxprog` to disable applying the maximum progress assumption during model building (for Markov Automata).
  72. - Added hybrid engine for Markov Automata.
  73. - Improved performance of the Unif+ algorithm (used for time-bounded properties on Markov Automata).
  74. - Various performance improvements for model building with the sparse engine.
  75. - `storm-dft`: Symmetry reduction is now enabled by default and can be disabled via `--nosymmetryreduction`.
  76. - `storm-pomdp`: Only accept POMDPs that are canonical.
  77. - `storm-pomdp`: Prism language extended with observable expressions.
  78. - `storm-pomdp`: Various fixes that prevented usage.
  79. - Several bug fixes.
  80. Version 1.4.x
  81. -------------
  82. ### Version 1.4.1 (2019/12)
  83. - Implemented long run average (LRA) computation for DTMCs/CTMCs via value iteration and via gain/bias equations.
  84. - Added several LRA related settings in a new settings module. Note that `--minmax:lramethod` has been replaced by `--lra:nondetmethod`.
  85. ### Version 1.4.0 (2019/11)
  86. - Added support for multi-dimensional quantile queries.
  87. - Added support for multi-objective model checking under pure (deterministic) schedulers with bounded memory using `--purescheds`.
  88. - Allow to quickly check a benchmark from the [Quantitative Verification Benchmark Set](http://qcomp.org/benchmarks/) using the `--qvbs` option.
  89. - Added script `resources/examples/download_qvbs.sh` to download the QVBS.
  90. - If an option is unknown, Storm now suggests similar option names.
  91. - Flagged several options as 'advanced' to clean up the `--help`-message. Use `--help all` to display a complete list of options.
  92. - Support for parsing of exact time bounds for properties, e.g., `P=? [F=27 "goal"]`.
  93. - Export of optimal schedulers when checking MDPs with the sparse engine (experimental). Use `--exportscheduler <filename>`.
  94. - PRISM language: Support for the new `round` operator.