DTMC Infinite reward

[diner]

Hi

I was trying to understand how the prob calculation works in PRISM. So I tried the example in this page:http://www.prismmodelchecker.org/casestudies/dice.php

Now when i try to find the prob of reaching a state, let's say when dice = 4, written in PCTL as P=? [F d=4], here d means dice, the result i get is ok (prob. equals to 1/6)

However the problem occurs when i try to find the time required to reach dice=4. for this i declared a reward structure that should assign reward of one to all the commands in the code.

rewards 

[] true: 1; //or only 'true:1' should also work

endrewards

But when i write the prop R = ? [F d=4], it gives me infinite reward. Why is that ? is there any way to count the expected value of required steps to reach dice = 4 ? 

thanks !

[Gethin Norman]

The reason you are getting infinity is that the probability of reaching a state where d=4 is less than 1. See the frequently asked questions:

http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties

thanks

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 https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.