Error: cannot take ceil() of Nan

Skip to first unread message

Ramesh Kumar

Feb 18, 2022, 8:40:09 AMFeb 18
to PRISM model checker
For the following PRISM code:


global R1:[11..50] init 30;
formula R1_drift_down2=ceil (min (pow(R1*R1-100,0.5), 50));
R1'= R1_drift_down2 // for certain conditions

I am getting the Error: cannot take ceil() of Nan: NaN is non-finite, cannot be represented by int

Anyway to resolve this?
Thank you.


Dave Parker

Apr 1, 2022, 3:35:09 AMApr 1
to, Ramesh Kumar
Hi Ramesh,

Your pow(...) expression is taking the square root of R1^2-100. In
places where R1^2-100 is negative, I guess this will result in NaN,
causing the error you saw.

Best wishes,

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to
> <>.
> To view this discussion on the web, visit
> <>.
Reply all
Reply to author
0 new messages