fixed properties for dice example

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@532 bbc10eb1-c90d-0410-af57-cb519fbb1720
18 years ago · 7cc4fec5a1
5 changed files with 8 additions and 14 deletions
--- a/prism-examples/dice/dice.pctl
+++ b/prism-examples/dice/dice.pctl
@ -9,5 +9,5 @@ P=? [ true U s=7 & d=6 ]
 // Probability of throwing x?
 P=? [ true U s=7 & d=x ]

-// Expected number of steps to complete?
+// Expected number of coin flips to complete?
 R=? [ F s=7 ]
--- a/prism-examples/dice/dice.pm
+++ b/prism-examples/dice/dice.pm
@ -18,8 +18,6 @@ module die
 	
 endmodule

-rewards
-	
-	true : 1;
-	
+rewards "coin_flips"
+	[] s<7 : 1;
 endrewards
--- a/prism-examples/dice/two_dice.nm
+++ b/prism-examples/dice/two_dice.nm
@ -20,8 +20,6 @@ endmodule

 module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule

-rewards
-	
-	true : 1;
-	
+rewards "coin_flips"
+	[] !(s1=7 & s2=7) : 1;
 endrewards
--- a/prism-examples/dice/two_dice_knuth.pctl
+++ b/prism-examples/dice/two_dice_knuth.pctl
@ -3,5 +3,5 @@ const int x;
 // probability of throwing x
 P=? [ true U s=34 & d=x ]

-// expected cost to complete
+// expected coin flips
 R=? [ F s=34 ]
--- a/prism-examples/dice/two_dice_knuth.pm
+++ b/prism-examples/dice/two_dice_knuth.pm
@ -45,8 +45,6 @@ module sum_of_two_dice
 	
 endmodule

-rewards
-	
-	true : 1;
-	
+rewards "coin_flips"
+	[] s<34 : 1;
 endrewards