Start to summarise changes in upcoming 4.1 release.

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

prism/CHANGELOG.txt

@@ -1,38 +1,45 @@
 This file contains details of the changes in each new version of PRISM.
 
 -----------------------------------------------------------------------------
-Latest changes (mostly reverse chronological):
-[correct wrt svn rev 6022]
+Version 4.1 (beta released ???)
 -----------------------------------------------------------------------------
 
-* GUI now takes both model and properties files as arguments
-* -importinit option works for steady-state as well as transient probability computation
-* Prototype reactions-to-PRISM translator
-* New options to plot graphs for simulation paths in the GUI
+* New explicit-state (pure Java) model checking engine
+  - coverage of much, but not all, of PRISM's model checking functionality
+  - new methods for MDPs: policy iteration (-politer) and Gauss-Seidel (-gs)
+  - accompanying major changes to underlying PRISM API
+
+* GUI improvements
+  - easy plotting of graphs for simulation paths in the GUI
+  - command-line GUI call (xprism)  takes both model and properties files as arguments
+  - easier zoom-out (double click) for graphs in GUI
+
+* Changes to deadlock handling:
+  - new option for "fix deadlocks" (defaults to *true*) (and new switch -nofixdl) 
+  - consistent deadlock handling everywhere, incl. GUI and experiments
+
+* Model checking improvements
+  - additional output in log of progress for numerical solution techniques
+  - -importinit option works for steady-state as well as transient probabilities
+  - new "printall" filter (shows zero results too, unlike "print")
+  - incremental computation of ranges of transient probabilities
+    when called from command-line (e.g. -tr 0.1:0.01:0.2) 
+
 * Improvements to simulation path generation using -simpath switch
   - more efficient path generation (on-the-fly) where possible
   - new 'snapshot' option to only show states at certain time-points
   - rewards are not displayed by default; use 'rewards' option to show
-* Easier zoom-out (double click) in graphs in GUI
-* Additional log output of progress for numerical solution techniques
-* Changes to PRISM default settings
+  
+* Changes to usage of PRISM settings file
   - settings file ~/.prism only read by GUI (not command-line) by default
   - new switch -settings to read a settings file from command-line PRISM
-* New switch -exportdigital for exporting PRISM code generated by digital clocks PTA engine
-* New scripts: prism-auto/prism-test/prism-filler
-* Added new "printall" filter.
+
 * Added viewing of witness/counterexample for E[F...] in GUI.
-* New syntax for transient probabilities in P operator: P=?[ F=T "target" ]
-* New (hidden) options for different symbolic reachability methods (-frontier, -bfs).
-* Command-line support for (incrementally) computing ranges of transient probabilities (e.g. -tr 0.1:0.01:0.2) 
+  
 * New file extensions: .prism, .props
-* Major changes to underlying PRISM API
-* Changes to deadlock handling:
-  - new option for "fix deadlocks" (defaults to *true*) (and new switch -fixdl) 
-  - consistent deadlock handling everywhere, incl. GUI and experiments
-  - changes to model-level deadlock storage (symbolic and explicit)
-* Explicit engine added as true engine, also available from GUI
-* New MDP solution methods (explicit engine only: ...) -politer
+* New scripts: prism-auto/prism-test/prism-filler
+* New -exportdigital switch for exporting PRISM code built by digital clocks PTA engine
+* New syntax for (CTMC) transient probabilities in P operator: P=?[ F=T "target" ]
 
 -----------------------------------------------------------------------------
 Version 4.0.3 (released 30/1/2012)