|
|
|
@ -1,41 +1,41 @@ |
|
|
|
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. |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
|
|
|
Latest changes (reverse chronological): |
|
|
|
|
|
|
|
* Transient probabilities computation for DTMCs |
|
|
|
* Sparse/hybrid versions of instantaneous reward properties (R=?[I=k]) for DTMCs |
|
|
|
* Added weak until (W) and release (R) to properties language |
|
|
|
* Easier viewing of model checking results in GUI |
|
|
|
* Steady-state properties/operators for DTMCs |
|
|
|
* GUI model editor: line numbers, undo |
|
|
|
* Language changes: no ranges, new function notation, semicolons, update parentheses |
|
|
|
* New parser: more efficient, better error reporting |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
Version 3.2.beta1 (released 25/2/2008) (svn: trunk rev 568) |
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
|
|
|
* Fix to allow building on Mac OS X v10.5 (Leopard) |
|
|
|
* New option for displaying extra info during reachability (-extrareachinfo switch) |
|
|
|
* Addition of some missing reward model checking algorithms |
|
|
|
- instantaneous reward properties (R=?[I=k]) for DTMCs/MDPs (MTBDD/sparse engines only) |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
|
|
|
Latest changes (reverse chronological): |
|
|
|
|
|
|
|
* Transient probabilities computation for DTMCs |
|
|
|
* Sparse/hybrid versions of instantaneous reward properties (R=?[I=k]) for DTMCs |
|
|
|
* Added weak until (W) and release (R) to properties language |
|
|
|
* Easier viewing of model checking results in GUI |
|
|
|
* Steady-state properties/operators for DTMCs |
|
|
|
* GUI model editor: line numbers, undo |
|
|
|
* Language changes: no ranges, new function notation, semicolons, update parentheses |
|
|
|
* New parser: more efficient, better error reporting |
|
|
|
|
|
|
|
----------------------------------------------------------------------------- |
|
|
|
Version 3.2.beta1 (released 25/2/2008) (svn: trunk rev 568) |
|
|
|
----------------------------------------------------------------------------- |
|
|
|
|
|
|
|
* Fix to allow building on Mac OS X v10.5 (Leopard) |
|
|
|
* New option for displaying extra info during reachability (-extrareachinfo switch) |
|
|
|
* Addition of some missing reward model checking algorithms |
|
|
|
- instantaneous reward properties (R=?[I=k]) for DTMCs/MDPs (MTBDD/sparse engines only) |
|
|
|
- cumulative reward properties (R=?[C<=k]) for DTMCs |
|
|
|
- sparse engine version of reach reward properties (R=?[F...]) for MDPs |
|
|
|
* New option for displaying extra (MT)BDD info (-extraddinfo switch) |
|
|
|
* Font increase/decrease feature in GUI |
|
|
|
* Labels (for use in properties file) can be defined in the model file |
|
|
|
* Properties files can use formulas from model file |
|
|
|
* Partially correct property files can be loaded into the GUI |
|
|
|
* New icon set and graphics |
|
|
|
* New graph plotting engine using JFreeChart |
|
|
|
* Prototype SBML-to-PRISM translator |
|
|
|
* New option for -simpath feature: can enable/disable loop checking |
|
|
|
* New option for -simpath feature: generation of multiple paths to find deadlock |
|
|
|
* New "rows" option for matrix exports (-exportrows switch) |
|
|
|
- sparse engine version of reach reward properties (R=?[F...]) for MDPs |
|
|
|
* New option for displaying extra (MT)BDD info (-extraddinfo switch) |
|
|
|
* Font increase/decrease feature in GUI |
|
|
|
* Labels (for use in properties file) can be defined in the model file |
|
|
|
* Properties files can use formulas from model file |
|
|
|
* Partially correct property files can be loaded into the GUI |
|
|
|
* New icon set and graphics |
|
|
|
* New graph plotting engine using JFreeChart |
|
|
|
* Prototype SBML-to-PRISM translator |
|
|
|
* New option for -simpath feature: can enable/disable loop checking |
|
|
|
* New option for -simpath feature: generation of multiple paths to find deadlock |
|
|
|
* New "rows" option for matrix exports (-exportrows switch) |
|
|
|
* Support for 64-bit architectures |
|
|
|
* Addition of F and G operators to property language (eventually/globally) |
|
|
|
* Redesign of the simulator GUI, plus new features: |
|
|
|
|
Dave Parker
18 years ago