From c17a50904dce939df7e46690284d787deea1616d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 6 Mar 2020 17:15:25 +0100 Subject: [PATCH] Updated CHANGELOG --- CHANGELOG.md | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6b4cb0017..ad40551f1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,20 +8,21 @@ Version 1.4.x ------------- ## Version 1.4.2 (under development) -- 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. ### Version 1.4.1 (2019/12)