diff --git a/prism/README.txt b/prism/README.txt index 913d6a7a..6ae664ea 100644 --- a/prism/README.txt +++ b/prism/README.txt @@ -94,7 +94,7 @@ Contributions to the development of PRISM have also been gratefully received fro * Paolo Ballarini & Kenneth Chan: Port of PRISM to Mac OS X * Rashid Mehmood: Improvements to low-level data structures and numerical solution algorithms * Alistair John Strachan, Mike Arthur and Zak Cohen: Integration of JFreeChart into PRISM - * Carlos Bederian (working with Pedro D'Argenio): Addition of LTL model checking for MDPs to PRISM + * Carlos Bederian (working with Pedro D'Argenio): Addition of LTL model checking for MDPs to PRISM For more details see: diff --git a/prism/VERSIONS.txt b/prism/VERSIONS.txt index 884ba2de..1df09f32 100644 --- a/prism/VERSIONS.txt +++ b/prism/VERSIONS.txt @@ -1,43 +1,43 @@ This file summarises the principal changes between each main public release of PRISM. For more detailed information about the various changes, see the file CHANGELOG.txt. ------------------------------------------------------------------------------ -Version 3.3.1 (released 22/11/2009) ------------------------------------------------------------------------------ - -* Minor bug fixes - +----------------------------------------------------------------------------- +Version 3.3.1 (released 22/11/2009) +----------------------------------------------------------------------------- + +* Minor bug fixes + ----------------------------------------------------------------------------- Version 3.3 (beta1 released 20/5/2009) ----------------------------------------------------------------------------- - -* 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) -* New tool features: + - 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) +* New tool features: - added symmetry reduction functionality - - steady-state/transient probability computation for DTMCs + - steady-state/transient probability computation for DTMCs - expanded cost/reward-property model checking support - - PRISM-to-html and PRISM-to-Latex conversion scripts - - efficiency improvements to precomputation algorithms - - BSCC export functionality (-exportbsccs switch) - - improvements to memory handling, especially in sparse/hybrid engines + - PRISM-to-html and PRISM-to-Latex conversion scripts + - efficiency improvements to precomputation algorithms + - BSCC export functionality (-exportbsccs switch) + - improvements to memory handling, especially in sparse/hybrid engines ----------------------------------------------------------------------------- Version 3.2 (beta released 25/2/2008)