|
|
|
@ -4,23 +4,24 @@ This file contains details of the changes in each new version of PRISM. |
|
|
|
Version 4.6 (first released 21/4/2020) |
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
|
|
|
New model checking features/enhancements: |
|
|
|
* New model checking features/enhancements: |
|
|
|
- digital clocks engine now supports time-bounded reachability |
|
|
|
- explicit engine support for steady-state computation (and S, R[S] properties) |
|
|
|
- improved support in MTBDD engine for very large (>2^63) state spaces |
|
|
|
- the -heuristic switch triggers automatic selection of some engines/settings |
|
|
|
- the -prop switch accepts multiple (comma-separated) property indices/names |
|
|
|
- MTBDD engine support for non-sparse vector printing (printall filter) |
|
|
|
- examples directory tidied up and now grouped by model type |
|
|
|
- many minor bugfixes |
|
|
|
|
|
|
|
New import/export features: |
|
|
|
* New import/export features: |
|
|
|
- export of result values for all states of a model (-exportvector) |
|
|
|
- basic auto-detection of model type for explicit file import |
|
|
|
- simulation (path generation and statistical model checking) for explicit model imports |
|
|
|
- explicit engine support for state reward import from files |
|
|
|
- MTBDD engine support for export of transient/steady-state probabilities |
|
|
|
|
|
|
|
* Examples directory tidied up and now grouped by model type |
|
|
|
|
|
|
|
* Development changes and enhancements: |
|
|
|
- extended/improved ModelGenerator interface, including methods to support simulation |
|
|
|
- new RewardGenerator interface for specifying information about rewards for a model |
|
|
|
|
Dave Parker
5 years ago