diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index dea4e64e..0df9672d 100644 --- a/prism/CHANGELOG.txt +++ b/prism/CHANGELOG.txt @@ -2,29 +2,10 @@ 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. +----------------------------------------------------------------------------- +Version 3.3.beta1 (released 20/5/2009) (svn: trunk rev 1066) ----------------------------------------------------------------------------- -Ongoing changes: - -* LTL model checking for MDPs -* CTL model checking - -Latest changes (reverse chronological): -[correct wrt svn rev 901] - -* 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 -* Initial state info for explicit import is now via -importlabels -* Added prism2html/prism2latex tools (in etc/scripts) -* Transient probabilities computation for DTMCs -* Sparse/hybrid versions of instantaneous reward properties (R=?[I=k]) for DTMCs -* Easier viewing of model checking results in GUI -* Steady-state properties/operators for DTMCs - * New language parser: - improved efficiency, especially on large/complex models - more accurate error reporting @@ -32,24 +13,35 @@ Latest changes (reverse chronological): - error highlighting - line numbers - undo/redo feature +* 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) -* Expanded property specification language - - arbitrary expressions allowed, e.g. 1-P=?[...] - - support got weak until (W) and release (R) added - - optional semicolons to terminate properties in properties files - - steady-state operators (S=?[...], R=?[S]) allowed for DTMCs * Other minor technical changes to language: - implication allowed in any expression (not just properties) - floor/ceil are now identifiers, not keywords - - equality and relational operators separated in priority - - precedence: >, <, >=, <= now have priority over =, != + - 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 +* Initial state info for explicit import is now via -importlabels +* 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 + ----------------------------------------------------------------------------- Version 3.2.beta1 (released 25/2/2008) (svn: trunk rev 568) ----------------------------------------------------------------------------- @@ -77,7 +69,8 @@ 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 ----------------------------------------------------------------------------- Version 3.1.1 (5/4/2007) (svn: derived from 3.1 tag) diff --git a/prism/README.txt b/prism/README.txt index 2e899adc..913d6a7a 100644 --- a/prism/README.txt +++ b/prism/README.txt @@ -2,7 +2,7 @@ README ====== -This is PRISM (Probabilistic Symbolic Model Checker), version 3.2. +This is PRISM (Probabilistic Symbolic Model Checker), version 3.3. ------------ INSTALLATION @@ -94,6 +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 For more details see: diff --git a/prism/VERSIONS.txt b/prism/VERSIONS.txt index 38ccf571..b2f7d21d 100644 --- a/prism/VERSIONS.txt +++ b/prism/VERSIONS.txt @@ -1,6 +1,38 @@ 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 (beta1 released 20/5/2009) +----------------------------------------------------------------------------- + +* New language parser: + - improved efficiency, especially on large/complex models + - more accurate error reporting +* 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=?[...] + - 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: + - added symmetry reduction functionality + - 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 + ----------------------------------------------------------------------------- Version 3.2 (beta released 25/2/2008) ----------------------------------------------------------------------------- diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index ad5a569d..5ae9da0e 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -47,7 +47,7 @@ import simulator.*; public class Prism implements PrismSettingsListener { // prism version - private static String version = "3.2.dev"; + private static String version = "3.3.beta1"; //------------------------------------------------------------------------------ // Constants