Support PRISM models with Intervals and CLI Extensions

[tquatmann]

This PR adds support for building prism models with intervals as documented here

It also extends/revises model-handling for CLI to incorporate intervals.

Addresses parts of #469

[tquatmann]

I had to do some more extensive CLI updates in model-handling.h to incorporate intervals as ValueType.

The old code had to set the right ValueTypes for model building and verification rather early.
This is becoming increasingly messy, in particular with the following things in mind:

• DRN models where we only realise during parsing whether intervals occur in the model
• Preprocessing that turn interval models into non-interval models or vice versa

We now use ModelBase (thus not requiring a ValueType) during the higher-level parts of model handling. The down-casting is done with some callback (castAndApply) mechanism. This required some changes in storm-pars and storm-pomdp, as well.

[tquatmann]

For testing the CLI re-implementation, I compiled a list of commands that should cover most of the functionality affected by this PR. I diffed the outputs for old vs. new implementation and manually checked that they are consistent.

Here is my command list for future reference.

set -e # fail on first error

STORMBIN=./build/bin
TESTFILES=./resources/examples/testfiles

$STORMBIN/storm;
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]'
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --prism2jani
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' -bisim
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --exact
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --exact -bisim
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --buildstateval --exportresult res.json; cat res.json; rm res.json
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P>0.5 [ F "one"]' --counterexample
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --exportbuild crowds5_5.drn; head -n20 crowds5_5.drn; rm crowds5_5.drn
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --exact --exportbuild crowds5_5.drn; head -n20 crowds5_5.drn; rm crowds5_5.drn
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine hybrid
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine hybrid --ddlib cudd
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine hybrid --exact
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd --exact
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd -bisim
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd -bisim --exact
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd-to-sparse
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine dd-to-sparse -bisim
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine automatic
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine expl
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine abs
$STORMBIN/storm --prism $TESTFILES/dtmc/die.pm --prop 'P=? [ F "one"]' --engine abs --abstraction:method games
$STORMBIN/storm --explicit-drn $TESTFILES/ma/jobscheduler.drn --prop 'Tmax=? [F "all_jobs_finished" ]'

$STORMBIN/storm --prism $TESTFILES/imdp/robot.prism -const delta=0.01 --buildfull;
$STORMBIN/storm --prism $TESTFILES/imdp/robot.prism -const delta=0.01 --buildfull --exportbuild robot.drn; cat robot.drn; rm robot.drn
$STORMBIN/storm --prism $TESTFILES/imdp/robot.prism -const delta=0.1 --buildfull --prop 'Pmax=? [F "goal1"]' --minmax:method vi;

$STORMBIN/storm-pars --prism $TESTFILES/pdtmc/parametric_die_2.pm --prop 'P=? [ F "one" ]' --mode solutionfunction
$STORMBIN/storm-pars --prism $TESTFILES/pdtmc/parametric_die_2.pm --prop 'P=? [ F "one" ]' --mode solutionfunction --engine dd

$STORMBIN/storm-pomdp --prism $TESTFILES/pomdp/maze2.prism -const sl=0 --prop 'Rmin=? [F "goal"]' --buildfull --belief-exploration
$STORMBIN/storm-pomdp --prism $TESTFILES/pomdp/maze2.prism -const sl=0 --prop 'Rmin=? [F "goal"]' --buildfull --belief-exploration --exact


echo "done"

[sjunges]

Hey Tim,

the fact that the expression-evaluator for state building does not take the interval but just the bounds into account (as far as I can see) confuses me a bit:

Does this mean that one can always evaluate the lower bound and the upper bound independently of each other? I am not sure if that works well for all kinds of operations, say 1/x with x in [-1,1] is not [-1,1] ?

[sjunges]

@linusheck did you look into this?

[sjunges]

This relates to #741

[sjunges]

I really like the changes in particular regarding the model handling :-)

[tquatmann]

Thanks for looking through this!

Does this mean that one can always evaluate the lower bound and the upper bound independently of each other? I am not sure if that works well for all kinds of operations, say 1/x with x in [-1,1] is not [-1,1] ?

Yes, lower bound and upper bound are evaluated independently. As far as I understand the PRISM specification this should be no issue as there are no expressions of type "interval". Please correct me if I'm wrong, though :)

[sjunges]

Thanks for looking through this!

Does this mean that one can always evaluate the lower bound and the upper bound independently of each other? I am not sure if that works well for all kinds of operations, say 1/x with x in [-1,1] is not [-1,1] ?

Yes, lower bound and upper bound are evaluated independently. As far as I understand the PRISM specification this should be no issue as there are no expressions of type "interval". Please correct me if I'm wrong, though :)

I see; the only arithmetic thus happens due to the composition/while flattening. As long as everything is nonnegative, this is not an issue.

[sjunges]

LGTM!