Skip to content

v4.7
Compare
Choose a tag to compare
@davexparker davexparker released this 23 Mar 23:40
· 480 commits to master since this release
v4.7
0c972a8

  • 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
Assets 6
Loading