Short-circuiting during model checking

[davexparker]

When evaluating Boolean operators (&, I, ?) in the context of a single state (or a constant), short-circuiting is applied. But during (explicit engine) model checking, where the expression evaluation is done recursively over the whole state vector, it is not. This stops ? being used to mask areas where an evaluation error might occur. For a contrived example:

 prism ../prism-examples/simple/dice/dice.pm -pf 's>0?pow(2,s-1):0' -ex

The same is true for the symbolic engines, but there the expression evaluation error checking is less robust, so the above example above does not generate an error. But neither does this, even though it should:

prism ../prism-examples/simple/dice/dice.pm -pf 'pow(2,s-1)' -m

and even though the error is partially detected and flagged with NaN:

prism ../prism-examples/simple/dice/dice.pm -pf 'filter(print,pow(2,s-1))' -m