From 0495f3bcb4d6f9dd90fdb5b55303fdd420a50995 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 4 Jul 2015 00:28:19 +0000 Subject: [PATCH] CHANGELOG. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10187 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/CHANGELOG.txt | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index edb009af..a8fd9471 100644 --- a/prism/CHANGELOG.txt +++ b/prism/CHANGELOG.txt @@ -1,24 +1,30 @@ This file contains details of the changes in each new version of PRISM. ----------------------------------------------------------------------------- -Version 4.2.2 (first released ???) +Version 4.3 (first released ???) ----------------------------------------------------------------------------- * Support for external LTL-to-automata converters via the HOA format -* Lower time-bounds for properties of DTMCs/MDPs (e.g. P=? [ F>=2 "target" ]) -* Arbitrary precision computation via the parametric engine (switch -exact) -* Expected total rewards (R[C]) implemented for DTMCs in symbolic engine -* Backwards reachability algorithm implemented for model checking PTAs -* Various LTL model checking optimisations -* New -pathviaautomata switch to force model checking via automaton construction -* New "comment" option for -exportresult switch (exports in regression test format) -* Changes to memory limits - - New -javamaxmem switch (equivalent to setting PRISM_JAVAMAXMEM) - - More convenient format for CUDD max memory setting (125k, 50m, 4g, etc.) - - Higher default values for CUDD/Java memory limits + +* New model checking functionality/optimisations + - lower time-bounds for properties of DTMCs/MDPs (e.g. P=? [ F>=2 "target" ]) + - arbitrary precision computation via the parametric engine (switch -exact) + - expected total rewards (R[C]) implemented for DTMCs in symbolic engine + - backwards reachability algorithm implemented for model checking PTAs + - various LTL model checking optimisations + +* Options/switches: + - new -pathviaautomata switch to force model checking via automaton construction + - new "comment" option for -exportresult switch (exports in regression test format) + - new -javamaxmem switch (equivalent to setting PRISM_JAVAMAXMEM) + - more convenient format for CUDD max memory setting (125k, 50m, 4g, etc.) + - higher default values for CUDD/Java memory limits + * Additional functionality in prism-auto testing/benchmarking script - - .auto files, export testing, debug mode, custom model files, ... + - export testing, .auto files, debug mode, custom model files, ... + * New sbml2prism script + * Bug fixes -----------------------------------------------------------------------------