- Added support for multi-objective model checking of long-run average objectives including mixtures with other kinds of objectives.
- Added support for generating optimal schedulers for globally formulae
- Simulator supports exact arithmetic
- Added switch
--no-simplify to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs)
- Fixed issues with JANI inputs concerning
- transient variable expressions in properties,
- constants in properties, and
- integer variables with either only an upper or only a lower bound.
storm-pomdp: States can be labelled with values for observable predicates
storm-pomdp: (Only API) Track state estimates
storm-pomdp: (Only API) Reduce computation of state estimates to computation on unrolled MDP