From 1c8bef7ae829e4ecb53a73a4ca092228eadea61c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 22 Jan 2010 16:46:38 +0000 Subject: [PATCH] CHANGELOG (update + formatting). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1706 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/CHANGELOG.txt | 146 ++++++++++++++++++++++---------------------- 1 file changed, 73 insertions(+), 73 deletions(-) diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index 7cac747c..7c4c9bbe 100644 --- a/prism/CHANGELOG.txt +++ b/prism/CHANGELOG.txt @@ -2,45 +2,45 @@ This file contains details of the changes in each new version of PRISM, including development and beta versions. For a less detailed overview of the main changes in each public release, see the file VERSIONS.txt. -Ongoing changes: - -* Explicit state libraries -* PTA model checking -* CTL model checking -* New simulator -* Adversary generation -* Access to action labels. inclusion in export, etc. -* Filters and propert semantics changes/additions - -Latest changes (reverse chronological): -[correct wrt svn rev 1610] - -* Formulas used in properties are left unexpanded for legibility -* New versions of jcommon (1.0.16) and jfreechart (1.0.13) -* Option to specify initial distribution for transient analysis -* Option to export transient probabilities to a file -* New -exporttransdotstates option -* Improved dot file export for MDPs -* Strict upper time-bounds allowed in properties -* New -exportprism switch -* Check for existence of zero-reward loops - -Temporary files: - -* NOTES* -* TODO -* examples/ - +Ongoing changes: + +* Explicit state libraries +* PTA model checking +* CTL model checking +* New simulator +* Adversary generation +* Access to action labels. inclusion in export, etc. +* Filters and propert semantics changes/additions + +Latest changes (reverse chronological): +[correct wrt svn rev 1610] + +* Formulas used in properties are left unexpanded for legibility +* New versions of jcommon (1.0.16) and jfreechart (1.0.13) +* Option to specify initial distribution for transient analysis +* Option to export transient probabilities to a file +* New -exporttransdotstates option +* Improved dot file export for MDPs +* Strict upper time-bounds allowed in properties +* New -exportprism switch +* Check for existence of zero-reward loops + +Temporary files: + +* NOTES* +* TODO +* examples/ + ----------------------------------------------------------------------------- Version 3.3.1 (released 22/11/2009) ----------------------------------------------------------------------------- - -Bug fixes: -- Building on new 64-bit Macs -- Simulator bug (crashes on min/max function) -- CTMC transient probs with MTBDD engine crash -- State/transition reward mix-up in parser -- Approximate verification of lower time-bounded properties for CTMCs + +Bug fixes: +- Building on new 64-bit Macs +- Simulator bug (crashes on min/max function) +- CTMC transient probs with MTBDD engine crash +- State/transition reward mix-up in parser +- Approximate verification of lower time-bounded properties for CTMCs ----------------------------------------------------------------------------- Version 3.3 (released 29/10/2009) @@ -49,56 +49,56 @@ Version 3.3 (released 29/10/2009) Bug fixes: - Building on new Macs - Copy+paste bug in GUI - + ----------------------------------------------------------------------------- Version 3.3.beta2 (released 29/7/2009) ------------------------------------------------------------------------------ +----------------------------------------------------------------------------- + +Bug fixes: +- LTL model checking (svn: 1112, 1132) +- Approximate model checking (svn: 1214) +- Building on new Macs (svn: 1103, 1105, 1349) -Bug fixes: -- LTL model checking (svn: 1112, 1132) -- Approximate model checking (svn: 1214) -- Building on new Macs (svn: 1103, 1105, 1349) - ----------------------------------------------------------------------------- Version 3.3.beta1 (released 20/5/2009) (svn: trunk rev 1066) ----------------------------------------------------------------------------- - -* New language parser: - - improved efficiency, especially on large/complex models + +* New language parser: + - improved efficiency, especially on large/complex models - more accurate error reporting -* GUI model editor improvements: - - error highlighting - - line numbers +* GUI model editor improvements: + - error highlighting + - line numbers - undo/redo feature -* Expanded property specification language - - LTL (and PCTL*) now supported - - arbitrary expressions allowed, e.g. 1-P=?[...] +* Expanded property specification language + - LTL (and PCTL*) now supported + - arbitrary expressions allowed, e.g. 1-P=?[...] - support for weak until (W) and release (R) added - - steady-state operators (S=?[...], R=?[S]) allowed for DTMCs - - optional semicolons to terminate properties in properties files -* Modelling language changes: - - cleaner notation for functions, e.g. mod(i,n), not func(mod,i,n) - - function names can be renamed in module renaming - - language strictness: updates (x'=...) must be parenthesised - - ranges (x=1..3,5) no longer supported - - added conversion tool for old models (etc/scripts/prism3to4) + - steady-state operators (S=?[...], R=?[S]) allowed for DTMCs + - optional semicolons to terminate properties in properties files +* Modelling language changes: + - cleaner notation for functions, e.g. mod(i,n), not func(mod,i,n) + - function names can be renamed in module renaming + - language strictness: updates (x'=...) must be parenthesised + - ranges (x=1..3,5) no longer supported + - added conversion tool for old models (etc/scripts/prism3to4) * Other minor technical changes to language: - - implication allowed in any expression (not just properties) - - floor/ceil are now identifiers, not keywords - - relational operators now have precedence over equality operators - - better but slightly different parsing of problem cases like "F<=a b" -* Improvements to memory handling, especially in sparse/hybrid engines -* Updated JFreeChart library -* Multiple -const switches allowed at command-line -* Efficiency improvements to precomputation algorithms + - implication allowed in any expression (not just properties) + - floor/ceil are now identifiers, not keywords + - relational operators now have precedence over equality operators + - better but slightly different parsing of problem cases like "F<=a b" +* Improvements to memory handling, especially in sparse/hybrid engines +* Updated JFreeChart library +* Multiple -const switches allowed at command-line +* Efficiency improvements to precomputation algorithms * Added symmetry reduction functionality -* New -exportbsccs option +* New -exportbsccs option * Initial state info for explicit import is now via -importlabels -* Added prism2html/prism2latex tools (in etc/scripts) +* Added prism2html/prism2latex tools (in etc/scripts) * Sparse/hybrid versions of instantaneous reward properties (R=?[I=k]) for DTMCs * Easier viewing of model checking results in GUI -* Steady-state/transient probability computation for DTMCs - +* Steady-state/transient probability computation for DTMCs + ----------------------------------------------------------------------------- Version 3.2.beta1 (released 25/2/2008) (svn: trunk rev 568) ----------------------------------------------------------------------------- @@ -126,7 +126,7 @@ Version 3.2.beta1 (released 25/2/2008) (svn: trunk rev 568) - ability to display cumulated time/rewards - new "Configure view" dialog - easier selection of next step (double click) -* Resizeable experiment results table +* Resizeable experiment results table * Function "log" for use in expressions -----------------------------------------------------------------------------