From dfcfb6c23f4f3e2cc2f7814c9e116cd170295136 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 16 Dec 2012 23:54:53 +0000 Subject: [PATCH] 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 | 51 ++++++++++++++++++++++++++------------------- 1 file changed, 29 insertions(+), 22 deletions(-) diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index af20de67..08622c91 100644 --- a/prism/CHANGELOG.txt +++ b/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)