From d784a87caa577a5a6cfe40dd7463a6dbb488c960 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 29 Jan 2012 21:16:02 +0000 Subject: [PATCH] Remove VERSIONS.txt - just use CHANGELOG.txt from now on. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4516 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/CHANGELOG.txt | 8 +- prism/VERSIONS.txt | 255 -------------------------------------------- 2 files changed, 3 insertions(+), 260 deletions(-) delete mode 100644 prism/VERSIONS.txt diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index 80e3399e..a74d8dc7 100644 --- a/prism/CHANGELOG.txt +++ b/prism/CHANGELOG.txt @@ -1,11 +1,9 @@ -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. +This file contains details of the changes in each new version of PRISM. +----------------------------------------------------------------------------- Latest changes (mostly reverse chronological): [correct wrt svn rev 4512] - -Changes: +----------------------------------------------------------------------------- * Property names - properties can be named, by prefixing with "name": diff --git a/prism/VERSIONS.txt b/prism/VERSIONS.txt deleted file mode 100644 index e9643713..00000000 --- a/prism/VERSIONS.txt +++ /dev/null @@ -1,255 +0,0 @@ -This file summarises the principal changes between each main public release of PRISM. -For more detailed information about the various changes, see the file CHANGELOG.txt. - ------------------------------------------------------------------------------ -Version 4.0.1 (released ...) ------------------------------------------------------------------------------ - -* Added if-and-only-if operator (<=>) for use in models/properties -* Updated version of explicit model checking library -* Testing mode (-test and -testall switches) -* Various bug fixes - ------------------------------------------------------------------------------ -Version 4.0 (beta released 16/12/2010) ------------------------------------------------------------------------------ - -* Support for probabilistic timed automata (PTAs) - - new modelling language features: clocks, invariants - - model checking of timed/untimed probabilistic reachability properties - - two model checking engines: abstraction-refinement, digital clocks - - support for expected reward properties (i.e. priced PTAs) - -* New approximate/statistical model checking functionality - - additional confidence-interval (CI) based approximation methods - - acceptance sampling: sequential probabilistic ratio test (SPRT) method - -* Optimal adversary generation for MDPs - - and for PTAs, via digital clocks engine - -* Improvements to the property language and model checking - - enhanced filters for property result processing - - new, clearer reporting of results from PRISM - -* Improved model export functionality - - option to include state information in dot files (e.g. -exporttransdotstates) - - action labels included in dot/transition matrix exports - - clearer for file export for MDPs - -* Additional functionality for transient/steady-state probabilities - - option to specify initial distribution for transient analysis - - option to export steady-state/transient probabilities to a file - -* New components/libraries for developers: - - completely re-written discrete-event simulation engine - - explicit-state probabilistic model checking library - - a quantitative abstraction-refinement engine - ------------------------------------------------------------------------------ -Version 3.3.1 (released 22/11/2009) ------------------------------------------------------------------------------ - -* Minor bug fixes - ------------------------------------------------------------------------------ -Version 3.3 (beta1 released 20/5/2009) ------------------------------------------------------------------------------ - -* New language parser: - - improved efficiency, especially on large/complex models - - more accurate error reporting - -* 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=?[...] - - 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) - -* New tool features: - - added symmetry reduction functionality - - steady-state/transient probability computation for DTMCs - - expanded cost/reward-property model checking support - - PRISM-to-html and PRISM-to-Latex conversion scripts - - efficiency improvements to precomputation algorithms - - BSCC export functionality (-exportbsccs switch) - - improvements to memory handling, especially in sparse/hybrid engines - ------------------------------------------------------------------------------ -Version 3.2 (beta released 25/2/2008) ------------------------------------------------------------------------------ - -* Support for 64-bit architectures and Mac OS X v10.5 (Leopard) - -* Improvements to property specification language - - addition of F and G operators (eventually/globally) - - can now use labels/formulas from model file in properties files - -* Redesign of the simulator GUI, plus new features: - - ability to display accumulated time/rewards - - new "Configure view" dialog - - easier selection of next step (double click) - -* New graph plotting engine using JFreeChart - -* Other GUI improvements: - - new icon set and graphics - - font increase/decrease feature - - loading of partially correct property files - -* Further additional functionality: - - extra reward model checking algorithms for some engines - - prototype SBML-to-PRISM translator - - new -exportrows switch for matrix exports - - new options for -simpath switch - - new -extraddinfo switch for displaying extra (MT)BDD info - ------------------------------------------------------------------------------ -Version 3.1.1 (released 5/4/2007) ------------------------------------------------------------------------------ - -* Minor bug fixes - ------------------------------------------------------------------------------ -Version 3.1 (released 15/11/2006) ------------------------------------------------------------------------------ - -* New installer for Windows binary -* Models can now have multiple (named) reward structures -* New -simpath switch for command-line generation of random paths with simulator -* Minor PRISM language improvements: - - type keyword does not need to be first thing in model file - - doubles in exponential form (1.4e-9) and unary minus (-1) allowed -* PRISM settings file now used by command-line version too -* Small GUI improvements -* New option to disable steady-state detection for CTMC transient analysis -* Bug fixes - ------------------------------------------------------------------------------ -Version 3.0 (released 6/7/2006) ------------------------------------------------------------------------------ - -* Discrete-event simulation engine added, providing: - - generation of approximate quantitative results via sampling - - debugging tool: manual model exploration and automatic trace generation - -* Support for costs and rewards: - - state-based and transition-based (impulse) costs/reward specification added to PRISM language - - verification (and simulation) of properties based on expected value of costs/rewards - (e.g. cumulated reward to reach state/time-bound, transient or steady-state reward value) - -* Overhaul of import/export functionality, including: - - export of transition matrix graph (Dot file) - - export of state/transition rewards - - export of property file labels and their satisfying states - - improved support for other export formats: Matlab, MRMC - - possibility to export to stdout/log instead of a file - - import of explicit model descriptions (from transition matrix and, optionally, state list) - -* GUI improvements, e.g.: - - additional graph plotting functionality - - XML-based import/export of graphs - - export of graphs to Matlab - -* Improved options management including saving of user settings -* Support for Mac OS X -* Easier compilation process -* Direct computation of transient probabilities -* Support for multiple initial states -* Improvements/additions to PRISM modelling/property languages -* Additional error checking on PRISM models -* Underlying data structure and efficiency improvements -* Bug fixes - ------------------------------------------------------------------------------ -Version 2.1 (released 8/9/2004) ------------------------------------------------------------------------------ - -* Now possible to build/run PRISM on Windows -* Compilation/installation procedures slightly simplified -* Splash screen on load - ------------------------------------------------------------------------------ -Version 2.0 (released 17/3/2004) ------------------------------------------------------------------------------ - -* Completely new graphical user interface, including: - - Text editor for PRISM language - - Automated results collection/graph plotting - -* Enhancements to PRISM language: - - Types (ints, doubles and booleans) and type checking added - - Probabilities/rates can now be expressions - - Variable ranges/initial values can now be expressions - - Constant/formula definitions can be expressions (including in terms of each other) - - Process algebra style definitions allowed for MDPs too (via "system" construct) - -* Enhancements to property specifications: - - Probability/time bounds in PCTL/CSL properties can now be expressions - - Use of constants now permitted: both those from the model and newly declared ones - - Added "init" keyword to PCTL/CSL (atomic proposition true only in initial state) - - Can define and reuse "labels" (atomic propositions) (like formulas in model files) - - Can write properties of the form "P=?[...]" which return the actual probability - - * Additional features: - - Automatic handling of multiple model checking computations, -e.g. check "P~p[true U<=k error]" for k=1..100 - - Added -exportstates switch, exports reachable states to text file - - Added -nobscc switch for optional bypass of BSCC computation - - Added explicit versions of export options (including first export option for MDPs) - - Export options can now be used in conjunction with each other and with model checking - - Added -version switch to display version - -* Efficiency improvements - - Improved heuristics for hybrid engine (sb/sbmax/gsl switches -> sbmax/sbl/gsmax/gsl) - - More efficient construction process for unstructured models - - General restructuring/improvements to model construction process implementation - -* Miscellaneous - - Various bug fixes - - Fairness (for MDP model checking) now OFF by default (used to be ON) - ------------------------------------------------------------------------------ -Version 1.3.1 (released 20/2/2003) ------------------------------------------------------------------------------ - -* Bug fixes in model construction code - ------------------------------------------------------------------------------ -Version 1.3 (released 10/2/2003) ------------------------------------------------------------------------------ - -* Steady-state probability computation improved to include strongly connected component (SCC) computation -* Extended support for CSL time-bounded until operator to include arbitrary intervals -* More flexible parallel composition options in the PRISM language (for DTMCs and CTMCs) -* Added option to import PEPA process algebra descriptions as models -* Improved range of numerical methods: (Backwards) Gauss-Seidel and (Backwards) SOR (plus variants for hybrid engine) -* Added -pctl/-csl switches to allow command line specification of properties -* Improved handling of deadlock states: can add self-loops to these states automatically (e.g. -fixdl switch) -* Steady-state probabilities are no longer automatically computed for CTMCs: use the -ss switch -* Addition of {} operator to PCTL/CSL formulas to support printing of probabilities -* Resolved problem with PRISM language syntax: updates must now be parenthesised -* Default value for maximum number of iterations reduced from 500,000 to (more sensible) 10,000 -* Added switches to control CUDD behaviour (-cuddmaxmem, -cuddepsilon) -* Additional example files -* Numerous bug fixlatest.htmles -* Now released under the GPL license - - ------------------------------------------------------------------------------ -Version 1.2 (released 17/9/2001) ------------------------------------------------------------------------------ - -First public release