Calculate expected values of “Craps Game” with the help of Prism Model Checker

I have modelled the craps game (https://en.wikipedia.org/wiki/Craps#Rules_of_play) as a dtmc with the prism model checker:

dtmc

module craps

// local state - won = 7, lost = 8
s : [0..8] init 0;

// first roll
[] s=0  -> 1/12: (s'=1)  +  // point 4
1/12: (s'=2)  +  // point 10
1/9 : (s'=3)  +  // point 5
1/9 : (s'=4)  +  // point 9
5/36: (s'=5)  +  // point 6
5/36: (s'=6)  +  // point 8
2/9 : (s'=7)  +  // won - point 7/11
1/9 : (s'=8);    // craps - point 2/3/12

// further rolls
[] s=1  ->   3/4 : (s'=1)  + 1/12 : (s'=7) + 1/6 : (s'=8);
[] s=2  ->   3/4 : (s'=2)  + 1/12 : (s'=7) + 1/6 : (s'=8);
[] s=3  -> 13/18 : (s'=3)  +  1/9 : (s'=7) + 1/6 : (s'=8);
[] s=4  -> 13/18 : (s'=4)  +  1/9 : (s'=7) + 1/6 : (s'=8);
[] s=5  -> 25/36 : (s'=5)  + 5/36 : (s'=7) + 1/6 : (s'=8);
[] s=6  -> 25/36 : (s'=6)  + 5/36 : (s'=7) + 1/6 : (s'=8);
[] s=7  -> (s'=7);
[] s=8  -> (s'=8);

endmodule

rewards "dice_rolls"
[] s<7 : 1;
endrewards


Now I need to calculate:

1. Creating a proper reward structure, calculate the expected number of rolls to win and to lose the game.
2. Creating a proper reward structure and considering a variant of the game in which at each roll of the dice a cost of 1 is payed by the player, calculate the expected money payed to reach a state of winning and the expected money payed to reach a state of loosing.

The reward structure "dice_rolls" should be good to calculate both the requirements, as IMHO they differ only semantically.

In the case of the expected number of rolls to win, a property like R=? [ F (s=7) ] gives as result Infinity , and the manual says "In the case where the probability of reaching a state satisfying prop is less than 1, the reward is equal to infinity"- http://www.prismmodelchecker.org/manual/PropertySpecification/Reward-basedProperties which (also intuitively) seems to confirm that the model is right (otherwise the dice would be not fair as there would be chances to win with P = 1.

Are my calculations right (the requested costs are all infinite), or I need to correct the reward structure and/or the reward property?

• It seems you're just looking for us to check that what you've done is correct. That isn't a good fit for the Stack Exchange format because it required detailed study of what you've done (rather than applying existing knowledge) and because the answer is unlikely to ever be interesting to anyone other than you. – David Richerby Mar 15 '17 at 15:04
• Well, that's a bit of point of view, do you want to me to rephrase the question by saying "given this Prism model" how do I calculate the expected number of rolls... with a proper reward structure"? Any questions of stackexchange is unlikely to ever be interesting to anyone other than the OP. – Markong Mar 15 '17 at 16:23
• Well, no, we don't particularly want you to rephrase the question as "solve this exercise for me". Rather, I suggest that you think about what prevents you from figuring out on your own whether your answer is correct. Is there some concept that you're unclear on? Can you edit your post to ask about a specific conceptual issue you're uncertain about? As a rule of thumb, a good conceptual question should be useful even to someone who isn't looking at the problem you happen to be working on. If you just need someone to check your work, you might seek out a friend, classmate, or teacher. – D.W. Mar 15 '17 at 17:53
• @Margeas Actually a huge number of SE questions are of interest to people other than the person who originally asked them. Almost every time I need to know how to do something with LaTeX or Mathematica, for example, the first Google hit is almost always to a Stack Exchange question where somebody's already asked the same thing and received an answer. One of the explicit goals of Stack Exchange is to build up a repository of high-quality questions and answers as a useful resource. – David Richerby Mar 15 '17 at 19:01