NaN probability from constant

[kleinj]

(with Linda Leuschner)

Consider the following PRISM DTMC:

dtmc

const double p  = pow(1 - 1E-7, 50);

module error
x : [0..2] init 0;

[] true  ->
     0.5 : true
  +  0.5 : (x' = 1)
  +  p*0 : (x' = 2);
endmodule

With the explicit engine, this results in a non-stochastic matrix, as the p*0 expression is translated to NaN during model building. If one plugs in the pow(...) expression directly in the transition, i.e.,

  +  pow(1 - 1E-7, 50)*0 : (x' = 2);

everything works fine. Exact evaluation of both variants generates the expected model as well.

From some debugging it looks like the constant expression is simplified to a rational number (RationalLiteralExpression, the value looks fine) and then somehow in the conversion to double / evaluation of p*0 something goes wrong. The *0 is not necessary for triggering this bug, p and 1-p as the transition probabilities are both evaluated to NaN as well... The value of p is ~0.999995, so there should be no problem with storage as a double. However, as a rational number, p has a large numerator and denominator.

Apart from fixing the concrete evaluation bug, it would probably make sense to add checks that the likelihood values generated in the model builders are not one of the infinities or NaN.

[cdehnert]

Fixed in the current master with the help of Joachim.