PRISM 4.4

[Dave Parker]

Dear all,

We are pleased to announce the release of PRISM version 4.4, now
available as a beta release from:

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

A list of the main new features is below. For more precise details, see
the changelog, linked from the download page.

* New model checking functionality:
- expected reward to satisfy a co-safe LTL formula (MDPs, D/CTMCs)
- 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)
- CTL model checking in the explicit engine
- non-probabilistic LTL model checking in the explicit engine
- instantaneous reward computation (Rmax/min[I=x]), explicit engine
- DTMC transient probability computation for the explicit engine

* Imports and exports:
- model import from explicit files for the explicit engine
- full import of labels during explicit model import (all engines)
- import of state rewards during explicit model import
- 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 specs
- prism-auto: new options/features
- DD debugging options: -dddebug and -ddtrace switches, ref counting
- new option -exportiterations for visualising iterative methods
- code base now allows/assumes Java 8

Best wishes,

Dave

[Debjani Ghosh]

Great!!

 

- better error handling when CUDD runs out of memory

 - GUI also supports -javamaxmem switch to set Java memory

- new option -exportiterations for visualising iterative methods

 - export of state rewards from explicit engine

- new ModelGenerator interface for specifying models programmatically

very interesting features

 

--
You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchecker+unsubscribe@googlegroups.com.
To post to this group, send an email to prismmodelchecker@googlegroups.com.
Visit this group at https://groups.google.com/group/prismmodelchecker.
For more options, visit https://groups.google.com/d/optout.