This file contains details of the changes in each new version of PRISM. ----------------------------------------------------------------------------- Version 4.3.1 (first released 26/5/2015) ----------------------------------------------------------------------------- * 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 result (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