Support for interval-based transitions in storm

[sjunges]

• Support interval-based models
• Support import/export to DRN
• Added Robust VI for MinMaxLinearSolver
• Various changes that allow doubles as result whereas the model consists of intervals.

In particular, it requires

• models can have interval-valued transitions
• models can be parsed and exported to DRN
• an update of carl, (done, see Interval operations carl-storm#14)
• control robustness via checktask
• check scheduler extraction
• checks to ensure that intervals are non-zero
• implementation of canHandle
• merging V1426 carl-storm#21
• some convenience functions to add uncertainty
• finished tests,

Things that I will currently not support. I track these in this issue: #469

• Explicit support for solving on DTMCs -- the DTMCs must be declared as MDPs
• Support for rewards
• Bounded reachability properties
• Topological VI
• Convenience functions to remove uncertainty (e.g., by taking the 'center').
• support for robustness in formulas
• Generating interval models from PRISM/JANI

Other things that I do not support and that I do not see happening right now

• DD-based representations
• Modified Policy iteration / LP-based methods
• Exact intervals

[sjunges]

@volkm The tests currently fail due to /opt/storm/src/storm/models/sparse/Ctmc.cpp:87:45: error: no match for 'operator/' (operand types are 'const storm::storage::MatrixEntry<long unsigned int, carl::Interval<double> >::value_type' {aka 'const carl::Interval<double>'} and 'const __gnu_cxx::__alloc_traits<std::allocator<carl::Interval<double> >, carl::Interval<double> >::value_type' {aka 'const carl::Interval<double>'}) Do you have any clue what is going on here? It looks also in carl/Interval.h, but does not check for the actually correct definition

It looks like this is an issue on the systems based on the debug basesystem. Could it be that they have a slightly outdated carl version? Do you build from tag or from head there?

[volkm]

Yes, the pre-built images use carl-storm:stable and not the latest head. I will update it and then trigger a rerun.

[sjunges]

stormchecker/carl-storm#21 must be merged first

[tquatmann]

Although interval support is still in its infancy, I think this is great progress! Thanks for all the effort :)

I have a few comments (mostly minor) and I added two PRs on your branch here and here

[sjunges]

@volkm @tquatmann I believe this is ready to be reviewed. I would value two pairs of eyes given the large number of essential files being touched.

[tquatmann]

LGTM (besides the minor issues I pointed out)

[volkm]

In general, it looks good to me. Thank you for all the work, in particular addingstorm::Interval and SolutionType in so many places.

I have two general comments:

• I would avoid the if interval { throw ..} else { } and just use if interval { throw} .... That way the else part does not have to be indented and less lines are changed. But this is my personal opinion.
• In a couple of places we still use assert(..) instead of STORM_LOG_ASSERT(..). But maybe this is more a general issue which could be addressed in a separate issue.

[sjunges]

@volkm I tried to remove the else parts, however, they are explicitly necessary right now to make it compile. I therefore ignore your suggestion :-)

[sjunges]

Once this passes all tests, I plan to squash and merge. Thanks for all the feedback.

[volkm]

@volkm I tried to remove the else parts, however, they are explicitly necessary right now to make it compile. I therefore ignore your suggestion :-)

In one instance the issue was just because there was still a dangling } from the else part.

But I am also fine with ignoring the comments.

[sjunges]

@volkm I tried to remove the else parts, however, they are explicitly necessary right now to make it compile. I therefore ignore your suggestion :-)

In one instance the issue was just because there was still a dangling } from the else part.

But I am also fine with ignoring the comments.

That was why the CI failed. But fixing that does not make the code compile.

Note that these are if constexpr (...). The code in the else block is only compiled for non-interval value types. That is essential, because e.g. there is no SoundValueIteration for storm::Interval.
By removing the else block, the code is compiled for storm::Interval, leading to compile errors.

[volkm]

You are fully right and now I understand the issue. Thanks for the explanation.

[volkm]

All my comments have been addressed. We can merge it.