Support for discounted properties in MDPs and DTMCs

[AlexBork]

This PR adds support for checking cumulative and total reward properties with a given discount factor on MDPs and DTMCs.

• Extends the parser to allow discounted properties, proposed syntax is R=? [Cdiscount=_factor_]
• Introduces helper classes for checking discounted properties
• Extends the respective PCTL model checking classes with support for discounted cumulative and total reward properties, implemented analogous to the existing undiscounted implementations

[sjunges]

This is absolutely great.

I have two questions:

• Does this code support convergence detection based on the Bellman residual error?
• Do we throw relevant error messages when doing, e.g., weak bismulation?

Best,
Sebastian

[AlexBork]

Yes, convergence is detected using the Bellman residual, see src/storm/solver/helper/DiscountedValueIterationHelper.cpp. I have also tested convergence using only the number of iterations as the criterion, i.e. letting the iteration run until it is guaranteed that we are precise enough. That was however highly inefficient as the number of iterations for guaranteed convergence is usually far larger than the actual number needed to reach the precision.

The error messages are not implemented, I will take care of it! I'm happy about any pointers where such problems might occur.

[AlexBork]

Thanks @sjunges for the review! I incorporated your comments now.

[sjunges]

Thanks! @tquatmann do you want to have a look before merging?