VERSIONS/CHANGELOG.

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

prism/CHANGELOG.txt

@@ -2,8 +2,9 @@ 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.
 
-Latest changes (mostly reverse chronological):
-[correct wrt svn rev 2286]
+-----------------------------------------------------------------------------
+Version 4.0.beta (released 16/12/2010)
+-----------------------------------------------------------------------------
 
 * Support for probabilistic timed automata (PTAs)
   - new modelling language features: clocks, invariants

prism/VERSIONS.txt

@@ -1,6 +1,41 @@
 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 4.0 (beta released 16/12/2010)
+-----------------------------------------------------------------------------
+
+* Support for probabilistic timed automata (PTAs)
+  - new modelling language features: clocks, invariants
+  - model checking of timed/untimed probabilistic reachability properties
+  - two model checking engines: abstraction-refinement, digital clocks
+  - support for expected reward properties (i.e. priced PTAs)
+
+* New approximate/statistical model checking functionality
+  - additional confidence-interval (CI) based approximation methods
+  - acceptance sampling: sequential probabilistic ratio test (SPRT) method
+
+* Optimal adversary generation for MDPs
+  - and for PTAs, via digital clocks engine
+  
+* Improvements to the property language and model checking
+  - enhanced filters for property result processing
+  - new, clearer reporting of results from PRISM
+
+* Improved model export functionality
+  - option to include state information in dot files (e.g. -exporttransdotstates)
+  - action labels included in dot/transition matrix exports
+  - clearer for file export for MDPs
+
+* Additional functionality for transient/steady-state probabilities
+  - option to specify initial distribution for transient analysis
+  - option to export steady-state/transient probabilities to a file
+
+* New components/libraries for developers:
+  - completely re-written discrete-event simulation engine
+  - explicit-state probabilistic model checking library
+  - a quantitative abstraction-refinement engine 
+
 -----------------------------------------------------------------------------
 Version 3.3.1 (released 22/11/2009)
 -----------------------------------------------------------------------------
@@ -14,22 +49,26 @@ 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
@@ -157,7 +196,7 @@ Version 2.0 (released 17/3/2004)
   
  * Additional features:
   - Automatic handling of multiple model checking computations,
-    e.g. check "P~p[true U<=k error]" for k=1..100    
+e.g. check "P~p[true U<=k error]" for k=1..100
   - Added -exportstates switch, exports reachable states to text file
   - Added -nobscc switch for optional bypass of BSCC computation
   - Added explicit versions of export options (including first export option for MDPs)