From 6850de1ab1ab2fc6a829a667364a0bbbb9d8ff13 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 17 Dec 2012 12:36:12 +0000 Subject: [PATCH] Tweak changelog. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6215 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/CHANGELOG.txt | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index 08622c91..3be89717 100644 --- a/prism/CHANGELOG.txt +++ b/prism/CHANGELOG.txt @@ -4,6 +4,8 @@ This file contains details of the changes in each new version of PRISM. Version 4.1 (beta released ???) ----------------------------------------------------------------------------- +* Multi-objective model checking for MDPs + * 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) @@ -14,16 +16,18 @@ Version 4.1 (beta released ???) - command-line GUI call (xprism) takes both model and properties files as arguments - easier zoom-out (double click) for graphs in GUI +* Non-probabilistic counterexample generation for CTL E[F ...] or A[G ...] + * 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) + - new "printall" filter (shows zero results too, unlike "print") + - -importinit option works for steady-state as well as transient probabilities + - additional output in log of progress for numerical solution techniques * Improvements to simulation path generation using -simpath switch - more efficient path generation (on-the-fly) where possible @@ -34,8 +38,6 @@ Version 4.1 (beta released ???) - settings file ~/.prism only read by GUI (not command-line) by default - new switch -settings to read a settings file from command-line PRISM -* Added viewing of witness/counterexample for E[F...] in GUI. - * New file extensions: .prism, .props * New scripts: prism-auto/prism-test/prism-filler * New -exportdigital switch for exporting PRISM code built by digital clocks PTA engine