CHANGELOG.

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

prism/CHANGELOG.txt

@@ -2,22 +2,22 @@ This file contains details of the changes in each new version of PRISM.
 
 Recent changes: (up to svn rev 12001)
 
-New model checking functionality:
-- expected reward to satisfy a co-safe LTL formula (all engines)
-- expected total reward (R[C] operator) for CTMCs
+* New model checking functionality:
+  - expected reward to satisfy a co-safe LTL formula (MDPs, D/CTMCs, all engines)
+  - expected total reward (R[C] operator) for CTMCs (all engines)
   - CTL model checking in the explicit engine
   - non-probabilistic LTL model checking in the explicit engine
   - instantaneous reward computation (Rmax/min[I=x]) in the explicit engine
   - DTMC transient probability computation for the explicit engine
 
-Imports and exports:
+* Imports and exports:
   - model import from explicit files for the explicit engine (-import... switches)
+  - full import of labels during explicit model import (all engines)
   - import of state rewards during explicit model import (symbolic engines)
-- export of models to .dot format via the -exportmodel switch
-- export of property automata to HOA format (-exportpropaut:hoa da.hoa)
   - export of state rewards from explicit engine
+  - export of models to .dot format via the -exportmodel switch
 
-Miscellaneous:
+* Miscellaneous:
   - built-in support for Nailgun client/server
   - new timeout feature (-timeout switch)
   - performance improvements in explicit engine
@@ -25,23 +25,13 @@ Miscellaneous:
   - better error handling when CUDD runs out of memory
   - various bug fixes and performance improvements
 
-Features for developers:
+* Features for developers:
   - new ModelGenerator interface for specifying models programmatically
   - extensions to test mode: complex expressions for RESULT specifications
   - prism-auto: new options (--show-warnings, --nailgun, --ngprism), multiple -x switches
   - DD debugging options: -dddebug and -ddtrace switches, improved ref count debugging
   - code base now allows/assumes Java 8
 
-
-
-
-
-
-* Partial support for multi-objective queries expressed as Boolean expressions
-* Allow <<>> and [[]] operators for MDP (only * or empty), all engines
-
-
-
 -----------------------------------------------------------------------------
 Version 4.3.1 (first released 26/5/2015)
 -----------------------------------------------------------------------------