v4.8.1

• Migrate to CUDD version 3
• Transition reward export (MDP-like models) for explicit engine
• Fix broken transient probability computation
• Updates/fixes in install/launch/testing scripts and build process
• New tests in etc/tests available for easier build tests
• New -javaversion switch to show Java version used
• New --print-failures switch for prism-auto
• Various bugfixes

v4.8

• Support for interval DTMC (IDTMC) and interval MDP (IMDP) model checking

• Improved strategy (policy) generation

  • switch -exportstrat exports to tra/dot/txt format
  • additional export options (restrict/reduce, states, reach)
  • strategy generation extended for bounded reachability, LTL, POMDPs
  • GUI support for generating, exporting and simulating strategies

• Other features/enhancements:

  • PTA model checking supports global/non-local variables
  • ModelGenerator interface now supports real-time models (e.g., PTAs)
  • new -javaparams switch to pass command-line arguments to JVM
  • prism-log-extract: new field 'dd_nodes' for model MTBDD size

• Import/export enhancements:

  • import of multiple (and named) reward structures
  • reward exports include header with name/type
  • new setting for model export precision (-exportmodelprecision)
  • new "proplabels" option for -exportmodel and -exportlabels
  • new -exportproplabels switch to export (just) properties file labels
  • explicit model import without -importmodel: prism model.all
  • results export to new formats: PRISM comment, dataframe
  • results import from dataframe format (-importresults or GUI)
  • observation export for POMDPs (-exportobs or GUI)

• Fixes / upgrades

  • compile fix for newer MacOS
  • library updates: JAS (2.7.90), Log4j (2.16.0), jhoafparser (1.1.1)
  • various bugfixes

• Development and code-level changes

  • automated testing via GitHub Actions
  • unit testing via JUnit
  • JavaCC upgraded from version 6.0 to 7.0
  • major refactoring:
    • generic model/reward classes
    • ASTElement deepCopy()
    • Expression evaluation
    • explicit.StateValues
    • Strategy and related classes
    • Modules2MTBDD

v4.7

• New model checking functionality

  • support for POMDP/POPTA model checking
  • support for LTS model checking
  • reporting of model checking accuracy

• Features/enhancements:

  • bounded properties (e.g. P<p) raise error if results are too inaccurate
  • improved model type auto-detection (MDP/PTA/LTS/POMDP/POPTA)
  • new -dir switch to set current working dir in command line and GUI
  • support HOA input (HOAF2DA) without a number-of-states header

• Fixes

  • fixed to compile on Java 14
  • fixed to compile on 64-bit Arm Linux/Mac
  • consistent treatment of negative/infinite/NaN rewards in symbolic/explicit engines
  • disable tree of model info in GUI

• Development and code-level changes

  • code base now allows/assumes Java 9
  • testing RESULT specifications can be intervals [a,b]
  • prism-log-extract: new (meta)fields: prog_name, prog_version, prog
  • ModelGenerator improvements: auto-generates VarList; stores module info
  • explicit model refactoring: more default implementations in interfaces
  • bugfixes & refactoring

v4.6

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

v4.5

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

v4.4

• 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