CHANGELOG.txt

This file contains details of the changes in each new version of PRISM.

-----------------------------------------------------------------------------

Latest changes (up to 517709e8):

* Allow testing RESULT specifications to be intervals [a,b]
* prism-log-extract: New (meta)fields: prog_name, prog_version, prog
* Fixed to compile on Java 14
* Add -dir switch to set current working dir in command line and GUI
* Consistent treatment of negative/infinite/NaN rewards in symbolic/explicit engines
* ModelGenerator improvements: auto-generates VarList; stores module info
* HOAF2DA: Support HOA input without a number-of-states header
* Disable tree of model info in GUI
* Support for LTS model checking
* Improved model type auto-detect when unspecified (MDP/PTA/LTS)
* Bugfixes & refactoring

-----------------------------------------------------------------------------
Version 4.6 (first released 21/4/2020)
-----------------------------------------------------------------------------
  
* New model checking features/enhancements:
  - digital clocks engine now supports time-bounded reachability
  - explicit engine support for steady-state computation (and S, R[S] properties)
  - improved support in MTBDD engine for very large (>2^63) state spaces
  - the -heuristic switch triggers automatic selection of some engines/settings
  - the -prop switch accepts multiple (comma-separated) property indices/names
  - MTBDD engine support for non-sparse vector printing (printall filter)
  - many minor bugfixes
  
* New import/export features:
  - export of result values for all states of a model (-exportvector)
  - basic auto-detection of model type for explicit file import
  - simulation (path generation and statistical model checking) for explicit model imports
  - explicit engine support for state reward import from files
  - MTBDD engine support for export of transient/steady-state probabilities

* Examples directory tidied up and now grouped by model type

* Development changes and enhancements:
  - extended/improved ModelGenerator interface, including methods to support simulation
  - new RewardGenerator interface for specifying information about rewards for a model
  - PRISM API improvements: properties can be parsed against the currently loaded model
  - Makefile improvements: better configurability of directiories
  - Makefile improvements: better handling of variables and sub-Makefiles, incl. CUDD
  - new release_source Makefile target for building source releases

* Benchmarking/testing changes and enhancements:
  - new prism-log-extract script for processing PRISM log files
  - prism-auto: new options/features (--log-subdirs, --filter-models, --args-list)

-----------------------------------------------------------------------------
Version 4.5 (first released 19/4/2019)
-----------------------------------------------------------------------------

* New features
  - add round function to language (rounds to nearest integer)
  - Java stack size can be set via command-line switch -javastack (or PRISM_JAVASTACKSIZE)
  - fractional values allowed for constants in -const switch and in GUI
  - allow rewards to be included in simulation paths exported from GUI (like for -simpath)

* Enhancements and fixes:
  - PRISM GUI settings file (.prism) moved to more standard locations
  - ITE supported in exact/parametric mode
  - various improvements to model checking in "exact" mode
  - bugfix for incorrect model construction during fast adaptive uniformisation
  - faster explicit construction of models with no labels
  - command-line -exportsteadystates switch implies -steadystate
  - GUI shortcuts: double-clicks for addition of constants, labels
  - fixed Mac launch scripts for Java 10 (removed -d64 and -d32)
  - improved auto switching between model checking engines in some cases
  - many minor bugfixes

* Development changes and enhancements:
  - alignment of source code releases and GitHub repos (some files moved to top-level)
  - move/simplify release building Makefile scripts (see GitHub wiki)
  - utility scripts for installing PRISM on fresh OSs (in etc/scripts)
  - HTML copy of manual now included in repo
  - make clean_all cleans external libs too, e.g. lpsolve
  - switch from javah (deprecated since Java 8) to javac for JNI header generation
  - launch scripts now use exec to start Java by default (PRISM_NO_EXEC=yes to revert)

* Benchmarking/testing changes and enhancements:
  - integration of prism-tests into main repo
  - fractions/exact numbers allowed in testing RESULT specs
  - Travis build config for continuous integration testing
  - prism-auto guesses ngprism location
  - prism-auto options: --skip-export-runs, --skip-duplicate-runs, --timeout
  - Makefile targets/settings: test, testsecho, testsfull, TESTS_ARGS, source-jar
  - NG_MAINCLASS setting for running PRISM in Nailgun server mode (prism -ng)

-----------------------------------------------------------------------------
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