Semantics for param/exact model checking of R=?[ F "target" ] in DTMC

[kleinj]

It looks like the param engine (and thus as well the -exact model checking mode) has a slightly different semantics regarding paths that never reach the target states.

In standard PRISM, those paths are assigned an accumulated reward of +infinity and as P<1[ F "target"], the result for R=?[ F "target" ] is +infinity. For param, it looks like those paths are assigned an accumulated reward of 0.

In general, it would probably be useful to provide a way to select the desired semantics, both for the standard PRISM engines and for the param/exact engines.

[davexparker]

The parametric engine currently ignores the possibility of not reaching target entirely. Which is a bug really. What it should do is a standard graph computation to identify states for which the answer should be infinite. In principle this is doable since parametric models are required to preserve graph structure for any valid parameter value (although this is not currently checked). The complication is extracting the graph structure - more precisely, you'd need to look at the expression defining the probability for a transition and check if it is non-zero.