- Added portfolio engine which picks a good engine (among other settings) based on features of the symbolic input
- Setting `--engine dd-to-sparse --bisimulation` now triggers extracting the sparse bisimulation quotiont
- JIT model building is now invoked via `--engine jit` (instead of `--jit`)
- DRN: support import of choice labelling
- Added portfolio engine which picks a good engine (among other settings) based on features of the symbolic input.
- Abort of Storm (via timeout or CTRL+C for example) is now gracefully handled. After an abort signal the program waits some seconds to output the result computed so far and terminates afterwards. A second signal immediately terminates the program.
- Setting `--engine dd-to-sparse --bisimulation` now triggers extracting the sparse bisimulation quotient.
- JIT model building is now invoked via `--engine jit` (instead of `--jit`).
- DRN: support import of choice labelling.
- Added option `--build:buildchoiceorig` to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. `--exportscheduler`).
- Apply the maximum progress assumption while building a Markov automata with the Dd engine.
- Added option `--build:nomaxprog` to disable applying the maximum progress assumption during model building (for Markov Automata)
- Added hybrid engine for Markov Automata
- Implemented optimistic value iteration for sound computations and used it as a default
- Implemented optimistic value iteration for sound computations and use it as a default.
- Unif+ for time bounded properties on Markov automata now computes results with relative precision. Use `--absolute` for the previous behavior.
- Various performance improvements for model building with the sparse engine
- `storm-dft`: Symmetry reduction is now enabled by default and can be disabled via `--nosymmetryreduction`
- `storm-pomdp`: Only accept POMDPs that are canonical
- `storm-pomdp`: Prism language extended with observable expressions
- Apply the maximum progress assumption while building a Markov automata with the Dd engine.
- Added option `--build:nomaxprog` to disable applying the maximum progress assumption during model building (for Markov Automata).
- Added hybrid engine for Markov Automata.
- Various performance improvements for model building with the sparse engine.
- `storm-dft`: Symmetry reduction is now enabled by default and can be disabled via `--nosymmetryreduction`.
- `storm-pomdp`: Only accept POMDPs that are canonical.
- `storm-pomdp`: Prism language extended with observable expressions.
- `storm-pomdp`: Various fixes that prevented usage.
Matthias Volk
5 years ago