Pre-3.3-release stuff.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1073 bbc10eb1-c90d-0410-af57-cb519fbb1720

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)

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:
 

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)
 -----------------------------------------------------------------------------

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