Rewards Precision

[jun...@in.tum.de]

Hello,

I have a prism MDP model with several rather small probability values (in the range of 1e-10). I am interested in reward properties of the type Rmin=? [ C <= X ] where X is in the range of 50. Unfortunately, with these small probabilities I usually get 0.0 as results for the expected rewards. I understood that this is probably due to rounding errors (as I get values >0 when I use larger probabilities). I experimented with the -epsilon and -cuddepsilon switches with no success.
I am working on a 64 bit platform and I am using the current development version (prism-4.2.1.dev.r9678).

Are there any more options I could consider? Does it make sense to experiment with the above switches even further? (I tried values down to 1e-60).

Thanks in advance for your assistance (and for providing this great tool!)
Maximilian

[Gethin Norman]

Maximilian,

I am not sure if this will help, but you could try increasing the reward values by multiplying them all by some fixed constant. To obtain the actual expected reward you would just need to divide the value obtained by this constant.

Gethin

> --
> 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 prismmodelchec...@googlegroups.com.
> To post to this group, send email to prismmod...@googlegroups.com.
> Visit this group at http://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[jun...@in.tum.de]

Gethin,

your suggestion solved my problem, thank you very much!
I only thought about the probabilities but never considered rounding problems in the rewards.

Regards,
Maximilian