Sebastian Junges

Changelog

1

Maintaining the changelog over concurrent PRs is annoying. Before the next release, the Changelog must be updated.

We use carl::formula in a few places. These can easily be replaced by our own expressions. This would reduce the amount of code from carl that we are using, which...

For sparse models, we have a graph analysis (`ConstraintCollector`) that provides the graph-preserving constraints. For DDs there is no such thing, and Storm emits a warning when exporting the solution...

As @volkm wrote: We are not using add_imported_library in the CMake file for soplex. This would resolve one instance of anohter flaw: https://github.com/moves-rwth/storm/issues/358

Prism parser: Player is a keyword for MDPs

2

Imho, player should only be a reserved keyword when parsing games. In particular, player is not a keyword for regular prism and thus, marking player as a keywords yields incompatibility...

Based on https://github.com/moves-rwth/stormpy/pull/154

We bind quite some vectors and sets, which are currently copied explicitly every time, see https://pybind11.readthedocs.io/en/stable/advanced/cast/stl.html. It may be good to think about this. Another problem is that for sets,...

Minor: Creating DFA with outputs=None fails.

1

The following code fails, which is slightly unexpected: ``` dfa1 = DFA( start=0, inputs={0, 1}, outputs=None, label=lambda s: (s % 4) == 3, transition=lambda s, c: (s + c) %...

The Highs MILP solver is freely available under an MIT license, hosted on github, and significantly seems to outperform GLPK, which is our current default. This makes it an interesting...

Size of the docker container

3

In our dockerfile, we currently use multiple layers with multiple compile commands. This generally leads to big docker containers. An open question is whether we can make these docker containers...