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:
- Creating a proper reward structure, calculate the expected number of rolls to win and to lose the game.
- 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"-
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?