v3.2.1

• Improved support for external libraries (Z3/Yices/PPL)
  • binaries installed for new versions and more OSs, including PPL on Windows
  • improved, more robust install mechanism
  • better documentation of library build process
• Merged latest changes from PRISM:

• updates/fixes in install/launch/testing scripts and build process

v3.2

• Symbolic (MTBDD) model checking of turn-based stochastic games (SMGs)
• Correlated and fair equilibria for CSGs
• Add instantaneous (I=k) and cumulative (C<=k) rewards for SMGs
• Merged latest changes from PRISM (up to v4.8) and extensions:
  • improved strategy generation (-exportstrat and GUI)
  • major code refactoring, e.g., generic model classes
• Refactoring of CSG related classes
• Various bugfixes + tidying

v3.1

• Add support for co-safe probabilistic LTL on STPGs/SMGs
• Add switch -lpscalefactor for LPs in zero-sum model checking
• Allow use of Yices for CSG equilibria computation (-smtsolver yices)
• Merged latest changes from PRISM (up to v4.7) and extensions:
  • reporting of model checking accuracy for STPGs/SMGs
  • model auto-detection for TPTGs
• Various bugfixes + tidying

v3.0

• Support for concurrent stochastic games (CSGs)
• Model checking for equilibria properties of CSGs
• Support for turn-based timed probabilistic games (TPTGs)
• Small change to SMG modelling: some actions can be be assigned to no player
• Merged latest changes from PRISM (up to v4.6)
• Various bugfixes

v2.1

• Merged latest changes from PRISM (up to v4.5 and slightly beyond),
  including directory rearrangement (some files moved to top-level)
• Examples and tests tidied up (now in prism-examples/smgs directory
  and prism-tests/functionality/verify/{smgs,smgs-multi})
• Simplified dependencies on the PPL library
  (in particular, local copies are stored, so binary releases are self-contained)
• Version number of PRISM-games properly reported/displayed
• Some compositional functionality moved into separate branch for now
• Various bugfixes