PRISM 4.7

[Dave Parker]

Dear all,

We are pleased to announce that version 4.7 of PRISM has just been
released, and is available from the website:

http://www.prismmodelchecker.org/download.php

Notably, this adds support for POMDPs (partially observable Markov
decision processes), improved computation/reporting of model checking
accuracy, and fixes to build on new OSs and Java releases.

A fuller list of changes is appended below.

Best wishes,

Dave


-----------------------------------------------------------------------------
Version 4.7 (first released 19/3/2021)
-----------------------------------------------------------------------------

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