|
@ -4,24 +4,30 @@ Changelog |
|
|
This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog. |
|
|
This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog. |
|
|
The releases of major and minor versions contain an overview of changes since the last major/minor update. |
|
|
The releases of major and minor versions contain an overview of changes since the last major/minor update. |
|
|
|
|
|
|
|
|
|
|
|
Version 1.1.x |
|
|
|
|
|
------------- |
|
|
|
|
|
Long run average computation via LRA, LP based MDP model checking, parametric model checking has an own binary |
|
|
|
|
|
|
|
|
Version 1.0.x |
|
|
|
|
|
------------------- |
|
|
|
|
|
|
|
|
|
|
|
### Version 1.0.2 (2017/5) |
|
|
|
|
|
|
|
|
### Version 1.1.0 (2017/8) |
|
|
|
|
|
|
|
|
- Fix for nested formulae |
|
|
|
|
|
- JANI: Explicit engine supports custom model compositions. |
|
|
|
|
|
- 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 |
|
|
|
|
|
|
|
|
- Support for long-run average rewards on MDPs and Markov automata using a value-iteration based approach. |
|
|
|
|
|
Then, using FORCE_POPCNT enables the use of the SSE 4.2 instruction |
|
|
|
|
|
- Parametric model checking is now handled in a separated library/executable called storm-pars. |
|
|
- Wellformedness constraints on PMCs: |
|
|
- Wellformedness constraints on PMCs: |
|
|
* include constraints from rewards |
|
|
* include constraints from rewards |
|
|
* are in smtlib2 |
|
|
* are in smtlib2 |
|
|
- 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 |
|
|
|
|
|
- Parametric model checking is now handled in a separated library/executable called storm-pars |
|
|
|
|
|
- Support for long-run average rewards on MDPs and Markov automata using a value-iteration based approach |
|
|
|
|
|
|
|
|
* 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. |
|
|
- 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. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Version 1.0.x |
|
|
|
|
|
------------- |
|
|
|
|
|
|
|
|
### Version 1.0.1 (2017/4) |
|
|
### Version 1.0.1 (2017/4) |
|
|
|
|
|
|
|
|