|
|
|
@ -7,9 +7,9 @@ The releases of major and minor versions contain an overview of changes since th |
|
|
|
Version 1.2.x |
|
|
|
------------- |
|
|
|
|
|
|
|
### Version 1.2.0 |
|
|
|
- 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 |
|
|
|
### Version 1.2.0 (2017/12) |
|
|
|
- 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 |
|
|
|
@ -22,9 +22,9 @@ Version 1.2.x |
|
|
|
- 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 |
|
|
|
- `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 |
|
|
|
@ -36,10 +36,9 @@ Version 1.1.x |
|
|
|
------------- |
|
|
|
|
|
|
|
### Version 1.1.0 (2017/8) |
|
|
|
|
|
|
|
- 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. |
|
|
|
- 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 |
|
|
|
@ -50,15 +49,14 @@ Version 1.1.x |
|
|
|
- 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 |
|
|
|
- `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 |
|
|
|
|
|
|
|
|
|
|
|
Version 1.0.x |
|
|
|
------------- |
|
|
|
|
|
|
|
### Version 1.0.1 (2017/4) |
|
|
|
|
|
|
|
- Multi-objective model checking support now fully included |
|
|
|
- Several improvements in parameter lifting |
|
|
|
- Several improvements in JANI parsing |
|
|
|
|
Matthias Volk
7 years ago