Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
682 lines (538 sloc) 30.1 KB
This file contains details of the changes in each new version of PRISM.
-----------------------------------------------------------------------------
Version 4.4 (first released 23/7/2017)
-----------------------------------------------------------------------------
* New model checking functionality:
- expected reward to satisfy a co-safe LTL formula (MDPs, D/CTMCs, all engines)
- interval iteration (MDPs, D/CTMCs, all engines)
- topological value iteration (MDPs, D/CTMCs, explicit engine)
- expected total reward (R[C] operator) for CTMCs and MDPs (max), all engines
- CTL model checking in the explicit engine
- non-probabilistic LTL model checking in the explicit engine
- instantaneous reward computation (Rmax/min[I=x]) in the explicit engine
- DTMC transient probability computation for the explicit engine
* Imports and exports:
- model import from explicit files for the explicit engine (-import... switches)
- full import of labels during explicit model import (all engines)
- import of state rewards during explicit model import (symbolic engines)
- export of state rewards from explicit engine
- export of models to .dot format via the -exportmodel switch
* Miscellaneous:
- built-in support for Nailgun client/server
- new timeout feature (-timeout switch)
- performance improvements in explicit engine
- GUI also supports -javamaxmem switch to set Java memory
- better error handling when CUDD runs out of memory
- various bug fixes and performance improvements
* Features for developers:
- new ModelGenerator interface for specifying models programmatically
- extensions to test mode: complex expressions for RESULT specifications
- prism-auto: new options/features (e.g., --show-warnings, --nailgun, --ngprism, --verbose-test)
- DD debugging options: -dddebug and -ddtrace switches, improved ref count debugging
- new option -exportiterations for visualising iterative numerical methods
- code base now allows/assumes Java 8
-----------------------------------------------------------------------------
Version 4.3.1 (first released 26/5/2016)
-----------------------------------------------------------------------------
* Bug fixes:
- launch scripts on OS X (especially El Capitan)
- lpsolve compile fix for recent Linux distributions
-----------------------------------------------------------------------------
Version 4.3 (first released 14/7/2015)
-----------------------------------------------------------------------------
* Support for external LTL-to-automata converters via the HOA format
- including model checking for Generalised Rabin (GR) conditions
* New model checking functionality/optimisations
- lower time-bounds for properties of DTMCs/MDPs (e.g. P=? [ F>=2 "target" ])
- expected total rewards (R[C]) implemented for DTMCs
- backwards reachability algorithm implemented for model checking PTAs
- exact (arbitrary precision) model checking via the parametric engine (experimental)
- various LTL model checking optimisations
- faster precomputation by pre-computing predecessors (explicit engine)
* Options/switches:
- new -pathviaautomata switch to force model checking via automaton construction
- new "comment" option for exporting results (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
- export testing, .auto files, debug mode, colouring, custom model files, ...
* New sbml2prism script
* Bug fixes
-----------------------------------------------------------------------------
Version 4.2.1 (first released 4/12/2014)
-----------------------------------------------------------------------------
* Bug fixes
-----------------------------------------------------------------------------
Version 4.2 (beta first released 12/5/2014)
-----------------------------------------------------------------------------
* Parametric model checking
* New model checking and export functionality
- fast adaptive uniformisation for CTMC transient analysis
- added R[C<=k] operator for MDPs (sparse, explicit)
- new -exportmecs and -exportsccs switches
- additional functionality in explicit engine (export BSCCs, LTL)
- improved adversary strategy generation in explicit engine
- integer variables can be unbounded (e.g. "x:int;"), for simulation-based analysis
* New options/switches:
- new -exportmodel and -importmodel convenience switches
- new -sumroundoff switch (used when checking probabilities sum to 1)
- some new '-help xxx' switches (const,simpath,exportresults,aroptions,exportmodel,importmodel)
- allow command-line switches of form --sw (as well as -sw)
- slight change to notation for -exportresults to match -exportmodel
* Additional functionality available in GUI:
- export steady-state/transient probabilities from GUI
- export/view labels from model/properties from GUI
- small improvements to usability of the GUI simulator transition table
- additional graph zoom functionality on popup menu
* Updates to build process
- fixed building on new versions of Cygwin (32/64-bit Windows)
- update CUDD to version 2.5.0
-----------------------------------------------------------------------------
Version 4.1 (first released 20/12/2012)
-----------------------------------------------------------------------------
* Multi-objective model checking for MDPs
* New explicit-state (pure Java) model checking engine
- coverage of much, but not all, of PRISM's model checking functionality
- new methods for MDPs: policy iteration (-politer -modpoliter) and Gauss-Seidel (-gs)
- accompanying significant changes to underlying PRISM (Java) API
* GUI improvements
- easy plotting of graphs for simulation paths in the GUI
- command-line GUI call (xprism) takes both model and properties files as arguments
- easier zoom-out (double click) for graphs in GUI
* CTL model checking (most operators)
- and counterexample/witness generation for A[G ...] or E[F ...]
* Changes to deadlock handling:
- new option for "fix deadlocks" (defaults to *true*) (and new switch -nofixdl)
- consistent deadlock handling everywhere, incl. GUI and experiments
* Model checking improvements
- incremental computation of ranges of transient probabilities
when called from command-line (e.g. -tr 0.1:0.01:0.2)
- new "printall" filter (shows zero results too, unlike "print")
- -importinit option works for steady-state as well as transient probabilities
- additional output in log of progress for numerical solution techniques
* Improvements to simulation path generation using -simpath switch
- more efficient path generation (on-the-fly) where possible
- new 'snapshot' option to only show states at certain time-points
- added 'probs' option to display transition probabilities/rates
- rewards are not displayed by default; use 'rewards' option to show
* Changes to usage of PRISM settings file
- settings file ~/.prism only read by GUI (not command-line) by default
- new switch -settings to read a settings file from command-line PRISM
* New file extensions for model/properties files: .prism, .props
* New scripts for testing and benchmarking: prism-auto/prism-test/prism-filler
* New -exportdigital switch for exporting PRISM code built by digital clocks PTA engine
* New syntax for (CTMC) transient probabilities in P operator: P=? [ F=T "target" ]
-----------------------------------------------------------------------------
Version 4.0.3 (released 30/1/2012)
-----------------------------------------------------------------------------
* Property names
- properties can be named, by prefixing with "name":
- properties can appear as sub-formulae of other properties using name references
- command-line -prop switch allows selection of property to check by name
* New options for results export
- export in matrix form, e.g. for surface plots
- export in CSV (rather than tab-separated) form
- expanded switch: -exportresults file[,opt1,opt2,...] with options: matrix,csv
* Automatic engine switching if numerical computation not supported
* Optimised Rabin automata for a few common LTL formulae
* Added -pf as a command-line switch alias for -pctl/-csl
* Add .props as a properties file extension (in GUI)
* New switches -noprob0/-noprob1 to disable individual precomputation algorithms
* Added prominence given to log warning messages in command-line/GUI
* GUI on Macs uses Cmd, not Ctrl
* Added PrismTest class to illustrate programmatic use of PRISM
* Command-line scripts can signal termination via growlnotify/notify-send
* Bash completion scripts + additional syntax highlighters
-----------------------------------------------------------------------------
Version 4.0.2 (released 9/10/2011)
-----------------------------------------------------------------------------
* Better handling of undefined constants in properties
* Added -exportprodtrans and -exportprodstates switches
* More improvements to explicit engine
* Simulator fix: ignores "max path length" for time-bounded properties
* Fixed to compile on Java 7
* Fixed anti-aliasing in GUI model editor
* Various bug fixes
-----------------------------------------------------------------------------
Version 4.0.1 (released 27/7/2011)
-----------------------------------------------------------------------------
* 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 (released 28/6/2011)
-----------------------------------------------------------------------------
* 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
* Other improvements/additions:
- Strict upper time-bounds allowed in properties
- Formulas used in properties are left unexpanded for legibility
- Added check for existence of zero-reward loops in MDPs
- New -exportprism/-exportprismconst/-nobuild switches
- New -exporttarget switch
- New versions of jcommon (1.0.16) and jfreechart (1.0.13)
* Changes since 4.0.beta2 (released 10/6/2011)
- None
* Changes since 4.0.beta (released 16/12/2010)
- Bug fixes: simulator, error messages, typos and 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
-----------------------------------------------------------------------------
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)
-----------------------------------------------------------------------------
Version 3.3.beta1 (released 20/5/2009) (svn: trunk rev 1066)
-----------------------------------------------------------------------------
* 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)
* 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
* Added symmetry reduction functionality
* New -exportbsccs option
* Initial state info for explicit import is now via -importlabels
* 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
-----------------------------------------------------------------------------
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)
* Support for 64-bit architectures
* Addition of F and G operators to property language (eventually/globally)
* Redesign of the simulator GUI, plus new features:
- ability to display cumulated time/rewards
- new "Configure view" dialog
- easier selection of next step (double click)
* Resizeable experiment results table
* Function "log" for use in expressions
-----------------------------------------------------------------------------
Version 3.1.1 (5/4/2007) (svn: derived from 3.1 tag)
-----------------------------------------------------------------------------
* Minor bug fixes:
- bug in "New Graph" dialog which fails on Java 6
- threading bug which can cause graph plotting to freeze
- fix to possible failure of Windows launch scripts
-----------------------------------------------------------------------------
Version 3.1 (15/11/2006) (svn: derived from 3.1.beta1 tag)
-----------------------------------------------------------------------------
* No changes
-----------------------------------------------------------------------------
Version 3.1.beta1 (3/11/2006) (svn: trunk rev 116)
-----------------------------------------------------------------------------
* 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 (6/7/2006) (svn: trunk rev 55)
-----------------------------------------------------------------------------
* Bug fixes
-----------------------------------------------------------------------------
Version 3.0.beta1 (29/3/2006) (svn: trunk rev 45)
-----------------------------------------------------------------------------
* Changes to export functionality
- transition matrix graph can be exported to a Dot file (-exporttransdot)
- can export state/transition rewards
- can export labels and their satisfying states
- can export to stdout/log instead of a file
- can export in MRMC format
- improved support for Matlab format export
- exported matrices now ordered by default (by row)
- new/rearranged command-line switches
* Added new options to Model|View menu in GUI
* Additional checks when parsing models:
- synchronous commands modifying globals
(now disallowed, previously just advised against)
- modification of local variables by another module
(previously detected later at build-time)
* Improvements/changes to explicit import functionality:
- -importstates understands Boolean variables now
- -importinit option added
- Default module variable (x) indexed from 0, not 1
* Non-convergence of iterative methods is an error, not a warning
* Changed layout of simulator transition table (4 -> 3 columns)
* Bugfixes
* Makefile improvements
-----------------------------------------------------------------------------
Version 2.1.dev11.sim8 (3/3/2006)
-----------------------------------------------------------------------------
* Bug fix: computation of powers in simulator
* Bug fix: calculation of transition rewards from multiple actions
* Bug fixes: loop detection and deadlocks in simulator
-----------------------------------------------------------------------------
Version 2.1.dev11.sim7 (5/1/2006)
-----------------------------------------------------------------------------
* Bug fixes, tidying
-----------------------------------------------------------------------------
Version 2.1.dev11.sim6 (16/12/2005)
-----------------------------------------------------------------------------
* Merged with simulator branch
* Improved options management including saving of user settings
-----------------------------------------------------------------------------
Version 2.1.dev11 (5/12/2005)
-----------------------------------------------------------------------------
Changes:
* Bugfixes in GUI syntax highlighting, esp. for large model files
* Bugfix: out-of-range initial values banned
-----------------------------------------------------------------------------
Version 2.1.dev10 (21/10/2005)
-----------------------------------------------------------------------------
Changes:
* GUI syntax highlighting restructure and efficiency improvement
* Bugfix/tidy in GUI experiments, esp. with Booleans
* Bugfix/improvements in modulo operations
* Improvements to checks of probabilities/rates, e.g. for NaN
* Ability to disable checks of probabilities/rates
-----------------------------------------------------------------------------
Version 2.1.dev9 (27/05/2005)
-----------------------------------------------------------------------------
Changes:
* Tidied up simulator code/stubs
* Graphical model editor disabled
-----------------------------------------------------------------------------
Version 2.1.dev8 (11/05/2005)
-----------------------------------------------------------------------------
Changes:
* Can now be built on OS X
* Makefile improvements including better OS detection
* Bug fix improving efficiency of BSCC computation
* Improved reporting of multiple missing constants
-----------------------------------------------------------------------------
Version 2.1.dev7 (22/2/2005)
-----------------------------------------------------------------------------
Changes:
* Graphical model editor (temporarily?) enabled
* Addition of simulator code and stubs
* Tweaked main Makefile: stops after first error
-----------------------------------------------------------------------------
Version 2.1.dev6 (18/2/2005)
-----------------------------------------------------------------------------
Changes:
* Bug fix - alphabet for default synchronisation is now derived syntactically
* Updates to some APMC code
-----------------------------------------------------------------------------
Version 2.1.dev5 (11/2/2005)
-----------------------------------------------------------------------------
Partially completed changes:
* PRISM Preprocessor
* Improved hybrid GS
* Improved syntax highlighting
Changes:
* Max memory for Java VM modifiable via PRISM_JAVAMAXMEM environment variable
* Reorganisation of Linux/Solaris launch scripts
* New notation for functions in PRISM language: func(f,x,y)
* New built-in functions in PRISM language (new notation only) - power(pow), modulo(mod)
* Upgrade to newest version of CUDD (2.4.0)
* GUI supports multi-line comments for properties
* Command-line override of model type allowed (-dtmc,-ctmc,-mdp switches)
* Tidy up of output generated by filters in P/S operators
* Added built-in label "deadlock", true in states where deadlocks fixed by PRISM
* Conditional evaluation operator now allows bracketless nesting, e.g. a?b:c?d:e
* Bug fixes
-----------------------------------------------------------------------------
Version 2.1.dev4 (21/1/2005)
-----------------------------------------------------------------------------
Changes:
* New syntax for transition rewards (within rewards construct)
* Bugfix in Prob1A precomputation algorithm
* Bugfix: disappearing "{min}"/"{max}" from P/R operators
* Numerous improvements to graph plotting tool
- Export of graphs to Matlab
- Import/export of graphs from/to XML
- Enhanced scale behaviour/options
- Improved editing of series properties/data
- Various bug fixes
* More thorough checks of commands during model construction
- each command must define transitions for all states satisfying guard
-----------------------------------------------------------------------------
Version 2.1.dev3 (17/11/2004)
-----------------------------------------------------------------------------
Partially completed changes:
* Graphical model editor significantly improved (but disabled for now)
Changes:
* Support for import of (explicit) transition matrix and state space
(command-line only, via -importtrans/-importstates switches (and -dtmc,-ctmc,-mdp))
* Improvements to graph plotting functionality
* Log in GUI now operates with a limited size buffer to avoid out-of-memory problems
-----------------------------------------------------------------------------
Version 2.1.dev2 (20/10/2004)
-----------------------------------------------------------------------------
Partially completed changes:
* Support for costs/rewards
- DTMC: R[F] H/S/M
- MDP: R[F] M ok, H partial
- CTMC: R[F] H/S/M, R[I=t] H/S/M, R[S] H/S/M, C[<=t] H/S/M
Changes:
* Added facility to compute transient probabilities
-----------------------------------------------------------------------------
Version 2.1.dev1 (7/10/2004)
-----------------------------------------------------------------------------
Partially completed changes:
* Support for costs/rewards
* Checks during model construction that rates are non-negative and probabilities sum to one
Changes:
* Multiple initial states init...endinit
* Support for displaying min/max of a range of probabilities using {} notation
* New "compact" storage schemes (distinct values only) added to sparse/hybrid engines
* Sparse storage schemes now use (more compact) counts instead of start indices for rows/cols
* True Gauss-Seidel algorithm for hybrid engine
* New switches (-pgs, -psor, -bpgs, -bpsor) to access hybrid "psuedo" methods
* Language modification: updates can be "true", i.e. no variables change
* Added conditional evaluation operator (cond ? then : else) to PRISM language
-----------------------------------------------------------------------------
Version 2.1 (released 8/9/2004)
-----------------------------------------------------------------------------
Changes:
* Now possible to build/run PRISM on Windows
* Compilation/installation procedures slightly simplified
* Splash screen on load
-----------------------------------------------------------------------------
Version 2.0 (released 17/3/2004)
-----------------------------------------------------------------------------
Changes:
* 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)
-----------------------------------------------------------------------------
Changes:
* Bug fixes in model construction code
-----------------------------------------------------------------------------
Version 1.3 (released 10/2/2003)
-----------------------------------------------------------------------------
Changes:
* 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 fixes
* Now released under the GPL license
-----------------------------------------------------------------------------
Version 1.2 (released 17/9/2001)
-----------------------------------------------------------------------------
First public release