From 7cc4fec5a11e49de886a49124fb648d2c409dbeb Mon Sep 17 00:00:00 2001
From: Gethin Norman <gethin.norman@glasgow.ac.uk>
Date: Mon, 26 Nov 2007 11:21:39 +0000
Subject: [PATCH] fixed properties for dice example

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@532 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism-examples/dice/dice.pctl           | 2 +-
 prism-examples/dice/dice.pm             | 6 ++----
 prism-examples/dice/two_dice.nm         | 6 ++----
 prism-examples/dice/two_dice_knuth.pctl | 2 +-
 prism-examples/dice/two_dice_knuth.pm   | 6 ++----
 5 files changed, 8 insertions(+), 14 deletions(-)

diff --git a/prism-examples/dice/dice.pctl b/prism-examples/dice/dice.pctl
index 91cc022b..05df91a1 100644
--- 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 ]
diff --git a/prism-examples/dice/dice.pm b/prism-examples/dice/dice.pm
index 6d7fd250..4a82208a 100644
--- 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
diff --git a/prism-examples/dice/two_dice.nm b/prism-examples/dice/two_dice.nm
index ed6b81e1..58732acb 100644
--- 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
diff --git a/prism-examples/dice/two_dice_knuth.pctl b/prism-examples/dice/two_dice_knuth.pctl
index 12a39c20..f951d556 100644
--- 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 ]
diff --git a/prism-examples/dice/two_dice_knuth.pm b/prism-examples/dice/two_dice_knuth.pm
index 7ee1c530..a29560b8 100644
--- 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