Warn when using time bound on discrete-time models

[volkm]

We received an error when trying to use a bounded until formula in the SparseMdpParameterLiftingModelChecker. Turns out that F<=4 is parsed as a time bound as default but the SparseMdpParameterLiftingModelChecker expects a step bound.
This issue does not occur for normal DTMC/MDP model checking because we never explicitly check for a time bound here and implicitly treats the time bound as step bound.

This PR now allows time bounds in the ParameterLiftingModelChecker.

In addition, we explicitly warn when using a time bound in discrete-time models. This will lead to a lot of warnings though, because we parse a bound as a time bound by default and only use a step bound when explicitly instructed via Fsteps<=4.
To reduce the number of warnings, we could add a post-processing step to the parsing where we automatically translate time bounds to step bounds on discrete-time models. Alternatively, we could also remove the warnings again if we think this is too confusing.

[sjunges]

Hey! Thanks for fixing. I am also thinking about the python-side here and then the preprocessing becomes even more difficult. I would maybe argue that any discrete-time verification algorithm should not distinguish between time and steps. Only in continuous-time models, we should make that distinction.

Alternatively, we could say that there is steps, time, and undefined, and we would force people using continuous-time models to be explicit on how they want to limt the horizon.

[tquatmann]

Hey! Thanks for fixing. I am also thinking about the python-side here and then the preprocessing becomes even more difficult. I would maybe argue that any discrete-time verification algorithm should not distinguish between time and steps. Only in continuous-time models, we should make that distinction.

Alternatively, we could say that there is steps, time, and undefined, and we would force people using continuous-time models to be explicit on how they want to limt the horizon.

Maybe steps, time, and default, where default=steps for discrete-time models and default=time for continuous-time? This will not break out-of-the-box PRISM compatibility while being explicit about things.

[volkm]

I had the same in mind as Tim. I would extend the TimeBoundType with default and then have steps, time, rewards and default where default can be handled according to the model type if used.