diff --git a/prism/VERSIONS.txt b/prism/VERSIONS.txt index 14954a37..4fa54229 100644 --- a/prism/VERSIONS.txt +++ b/prism/VERSIONS.txt @@ -1,414 +1,207 @@ -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 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 - +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 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