|
|
|
@ -2,45 +2,45 @@ This file contains details of the changes in each new version of PRISM, |
|
|
|
including development and beta versions. For a less detailed overview |
|
|
|
of the main changes in each public release, see the file VERSIONS.txt. |
|
|
|
|
|
|
|
Ongoing changes: |
|
|
|
|
|
|
|
* Explicit state libraries |
|
|
|
* PTA model checking |
|
|
|
* CTL model checking |
|
|
|
* New simulator |
|
|
|
* Adversary generation |
|
|
|
* Access to action labels. inclusion in export, etc. |
|
|
|
* Filters and propert semantics changes/additions |
|
|
|
|
|
|
|
Latest changes (reverse chronological): |
|
|
|
[correct wrt svn rev 1610] |
|
|
|
|
|
|
|
* Formulas used in properties are left unexpanded for legibility |
|
|
|
* New versions of jcommon (1.0.16) and jfreechart (1.0.13) |
|
|
|
* Option to specify initial distribution for transient analysis |
|
|
|
* Option to export transient probabilities to a file |
|
|
|
* New -exporttransdotstates option |
|
|
|
* Improved dot file export for MDPs |
|
|
|
* Strict upper time-bounds allowed in properties |
|
|
|
* New -exportprism switch |
|
|
|
* Check for existence of zero-reward loops |
|
|
|
|
|
|
|
Temporary files: |
|
|
|
|
|
|
|
* NOTES* |
|
|
|
* TODO |
|
|
|
* examples/ |
|
|
|
|
|
|
|
Ongoing changes: |
|
|
|
|
|
|
|
* Explicit state libraries |
|
|
|
* PTA model checking |
|
|
|
* CTL model checking |
|
|
|
* New simulator |
|
|
|
* Adversary generation |
|
|
|
* Access to action labels. inclusion in export, etc. |
|
|
|
* Filters and propert semantics changes/additions |
|
|
|
|
|
|
|
Latest changes (reverse chronological): |
|
|
|
[correct wrt svn rev 1610] |
|
|
|
|
|
|
|
* Formulas used in properties are left unexpanded for legibility |
|
|
|
* New versions of jcommon (1.0.16) and jfreechart (1.0.13) |
|
|
|
* Option to specify initial distribution for transient analysis |
|
|
|
* Option to export transient probabilities to a file |
|
|
|
* New -exporttransdotstates option |
|
|
|
* Improved dot file export for MDPs |
|
|
|
* Strict upper time-bounds allowed in properties |
|
|
|
* New -exportprism switch |
|
|
|
* Check for existence of zero-reward loops |
|
|
|
|
|
|
|
Temporary files: |
|
|
|
|
|
|
|
* NOTES* |
|
|
|
* TODO |
|
|
|
* examples/ |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
Version 3.3.1 (released 22/11/2009) |
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
|
|
|
Bug fixes: |
|
|
|
- Building on new 64-bit Macs |
|
|
|
- Simulator bug (crashes on min/max function) |
|
|
|
- CTMC transient probs with MTBDD engine crash |
|
|
|
- State/transition reward mix-up in parser |
|
|
|
- Approximate verification of lower time-bounded properties for CTMCs |
|
|
|
|
|
|
|
Bug fixes: |
|
|
|
- Building on new 64-bit Macs |
|
|
|
- Simulator bug (crashes on min/max function) |
|
|
|
- CTMC transient probs with MTBDD engine crash |
|
|
|
- State/transition reward mix-up in parser |
|
|
|
- Approximate verification of lower time-bounded properties for CTMCs |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
Version 3.3 (released 29/10/2009) |
|
|
|
@ -49,56 +49,56 @@ Version 3.3 (released 29/10/2009) |
|
|
|
Bug fixes: |
|
|
|
- Building on new Macs |
|
|
|
- Copy+paste bug in GUI |
|
|
|
|
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
Version 3.3.beta2 (released 29/7/2009) |
|
|
|
----------------------------------------------------------------------------- |
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
|
|
|
Bug fixes: |
|
|
|
- LTL model checking (svn: 1112, 1132) |
|
|
|
- Approximate model checking (svn: 1214) |
|
|
|
- Building on new Macs (svn: 1103, 1105, 1349) |
|
|
|
|
|
|
|
Bug fixes: |
|
|
|
- LTL model checking (svn: 1112, 1132) |
|
|
|
- Approximate model checking (svn: 1214) |
|
|
|
- Building on new Macs (svn: 1103, 1105, 1349) |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
Version 3.3.beta1 (released 20/5/2009) (svn: trunk rev 1066) |
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
|
|
|
* New language parser: |
|
|
|
- improved efficiency, especially on large/complex models |
|
|
|
|
|
|
|
* New language parser: |
|
|
|
- improved efficiency, especially on large/complex models |
|
|
|
- more accurate error reporting |
|
|
|
* GUI model editor improvements: |
|
|
|
- error highlighting |
|
|
|
- line numbers |
|
|
|
* GUI model editor improvements: |
|
|
|
- error highlighting |
|
|
|
- line numbers |
|
|
|
- undo/redo feature |
|
|
|
* Expanded property specification language |
|
|
|
- LTL (and PCTL*) now supported |
|
|
|
- arbitrary expressions allowed, e.g. 1-P=?[...] |
|
|
|
* Expanded property specification language |
|
|
|
- LTL (and PCTL*) now supported |
|
|
|
- arbitrary expressions allowed, e.g. 1-P=?[...] |
|
|
|
- support for weak until (W) and release (R) added |
|
|
|
- steady-state operators (S=?[...], R=?[S]) allowed for DTMCs |
|
|
|
- optional semicolons to terminate properties in properties files |
|
|
|
* Modelling language changes: |
|
|
|
- cleaner notation for functions, e.g. mod(i,n), not func(mod,i,n) |
|
|
|
- function names can be renamed in module renaming |
|
|
|
- language strictness: updates (x'=...) must be parenthesised |
|
|
|
- ranges (x=1..3,5) no longer supported |
|
|
|
- added conversion tool for old models (etc/scripts/prism3to4) |
|
|
|
- steady-state operators (S=?[...], R=?[S]) allowed for DTMCs |
|
|
|
- optional semicolons to terminate properties in properties files |
|
|
|
* Modelling language changes: |
|
|
|
- cleaner notation for functions, e.g. mod(i,n), not func(mod,i,n) |
|
|
|
- function names can be renamed in module renaming |
|
|
|
- language strictness: updates (x'=...) must be parenthesised |
|
|
|
- ranges (x=1..3,5) no longer supported |
|
|
|
- added conversion tool for old models (etc/scripts/prism3to4) |
|
|
|
* Other minor technical changes to language: |
|
|
|
- implication allowed in any expression (not just properties) |
|
|
|
- floor/ceil are now identifiers, not keywords |
|
|
|
- relational operators now have precedence over equality operators |
|
|
|
- better but slightly different parsing of problem cases like "F<=a b" |
|
|
|
* Improvements to memory handling, especially in sparse/hybrid engines |
|
|
|
* Updated JFreeChart library |
|
|
|
* Multiple -const switches allowed at command-line |
|
|
|
* Efficiency improvements to precomputation algorithms |
|
|
|
- implication allowed in any expression (not just properties) |
|
|
|
- floor/ceil are now identifiers, not keywords |
|
|
|
- relational operators now have precedence over equality operators |
|
|
|
- better but slightly different parsing of problem cases like "F<=a b" |
|
|
|
* Improvements to memory handling, especially in sparse/hybrid engines |
|
|
|
* Updated JFreeChart library |
|
|
|
* Multiple -const switches allowed at command-line |
|
|
|
* Efficiency improvements to precomputation algorithms |
|
|
|
* Added symmetry reduction functionality |
|
|
|
* New -exportbsccs option |
|
|
|
* New -exportbsccs option |
|
|
|
* Initial state info for explicit import is now via -importlabels |
|
|
|
* Added prism2html/prism2latex tools (in etc/scripts) |
|
|
|
* Added prism2html/prism2latex tools (in etc/scripts) |
|
|
|
* Sparse/hybrid versions of instantaneous reward properties (R=?[I=k]) for DTMCs |
|
|
|
* Easier viewing of model checking results in GUI |
|
|
|
* Steady-state/transient probability computation for DTMCs |
|
|
|
|
|
|
|
* Steady-state/transient probability computation for DTMCs |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
Version 3.2.beta1 (released 25/2/2008) (svn: trunk rev 568) |
|
|
|
----------------------------------------------------------------------------- |
|
|
|
@ -126,7 +126,7 @@ Version 3.2.beta1 (released 25/2/2008) (svn: trunk rev 568) |
|
|
|
- ability to display cumulated time/rewards |
|
|
|
- new "Configure view" dialog |
|
|
|
- easier selection of next step (double click) |
|
|
|
* Resizeable experiment results table |
|
|
|
* Resizeable experiment results table |
|
|
|
* Function "log" for use in expressions |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
Dave Parker
16 years ago