v1.5.0

• 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).
• Implemented optimistic value iteration for sound computations and set it as new default in --sound mode.
• Time bounded properties for Markov automata are now computed with relative precision. Use --absolute for the previous behavior.
• Apply the maximum progress assumption while building a Markov automaton with one of the symbolic engines.
• Added option --build:nomaxprog to disable applying the maximum progress assumption during model building (for Markov Automata).
• Added hybrid engine for Markov Automata.
• Improved performance of the Unif+ algorithm (used for time-bounded properties on 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.
• Several bug fixes.