|
|
|
@ -1,24 +1,30 @@ |
|
|
|
This file contains details of the changes in each new version of PRISM. |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
Version 4.2.2 (first released ???) |
|
|
|
Version 4.3 (first released ???) |
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
|
|
|
* Support for external LTL-to-automata converters via the HOA format |
|
|
|
* Lower time-bounds for properties of DTMCs/MDPs (e.g. P=? [ F>=2 "target" ]) |
|
|
|
* Arbitrary precision computation via the parametric engine (switch -exact) |
|
|
|
* Expected total rewards (R[C]) implemented for DTMCs in symbolic engine |
|
|
|
* Backwards reachability algorithm implemented for model checking PTAs |
|
|
|
* Various LTL model checking optimisations |
|
|
|
* New -pathviaautomata switch to force model checking via automaton construction |
|
|
|
* New "comment" option for -exportresult switch (exports in regression test format) |
|
|
|
* Changes to memory limits |
|
|
|
- New -javamaxmem switch (equivalent to setting PRISM_JAVAMAXMEM) |
|
|
|
- More convenient format for CUDD max memory setting (125k, 50m, 4g, etc.) |
|
|
|
- Higher default values for CUDD/Java memory limits |
|
|
|
|
|
|
|
* New model checking functionality/optimisations |
|
|
|
- lower time-bounds for properties of DTMCs/MDPs (e.g. P=? [ F>=2 "target" ]) |
|
|
|
- arbitrary precision computation via the parametric engine (switch -exact) |
|
|
|
- expected total rewards (R[C]) implemented for DTMCs in symbolic engine |
|
|
|
- backwards reachability algorithm implemented for model checking PTAs |
|
|
|
- various LTL model checking optimisations |
|
|
|
|
|
|
|
* Options/switches: |
|
|
|
- new -pathviaautomata switch to force model checking via automaton construction |
|
|
|
- new "comment" option for -exportresult switch (exports in regression test format) |
|
|
|
- new -javamaxmem switch (equivalent to setting PRISM_JAVAMAXMEM) |
|
|
|
- more convenient format for CUDD max memory setting (125k, 50m, 4g, etc.) |
|
|
|
- higher default values for CUDD/Java memory limits |
|
|
|
|
|
|
|
* Additional functionality in prism-auto testing/benchmarking script |
|
|
|
- .auto files, export testing, debug mode, custom model files, ... |
|
|
|
- export testing, .auto files, debug mode, custom model files, ... |
|
|
|
|
|
|
|
* New sbml2prism script |
|
|
|
|
|
|
|
* Bug fixes |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
Dave Parker
11 years ago