From d7db1b4645f418e033d90d90f7a4768526f37942 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 5 Apr 2007 10:57:51 +0000
Subject: [PATCH] Update to cluster to use named reward structures.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@251 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism-examples/cluster/cluster.csl | 16 +++++++---------
 prism-examples/cluster/cluster.sm  | 27 +++++++++++++++------------
 2 files changed, 22 insertions(+), 21 deletions(-)

diff --git a/prism-examples/cluster/cluster.csl b/prism-examples/cluster/cluster.csl
index 334293dc..a328296d 100644
--- a/prism-examples/cluster/cluster.csl
+++ b/prism-examples/cluster/cluster.csl
@@ -5,9 +5,11 @@
 // operational_i : (left_n+right_n)>=i & Toleft_n & line_n & Toright_n
 // minimum_k : left_operational_k | right_operational_k | operational_k
 // premium = minimum_N
-const double T;
+
 label "minimum" = (left_n>=k & Toleft_n) | (right_n>=k & Toright_n) | ((left_n+right_n)>=k & Toleft_n & line_n & Toright_n);
 label "premium" = (left_n>=left_mx & Toleft_n) | (right_n>=right_mx & Toright_n) | ((left_n+right_n)>=left_mx & Toleft_n & line_n & Toright_n);
+
+const double T;
 
 // in the long run, the probability that premium QOS will be delivered
 S=? [ "premium" ]
@@ -28,20 +30,16 @@ P=? [ true U[T,T] !"minimum"  {!"minimum"}{max} ]
 P=? [ true U<=T "premium" {"minimum"}{min} ]
 
 // the minimum probability of going from minimum QOS to premium QOS within T time units without violating the minimum QOS constraint along the way
-P=? [ "minimum" U<=T "premium" {"minimum"}{min}]
+P=? [ "minimum" U<=T "premium" {"minimum"}{min} ]
 
 // the maximum probability that it takes more than T time units to recover from insufficient QOS
 P=? [ !"minimum" U>=T "minimum" {!"minimum"}{max} ]
 
 // percentage of operational workstations at time T starting from below minimum QOS
-// (set OPERATIONAL to true, MINIMUM to 0 and REPAIR to false)
-R=?[I=T {!"minimum"}{min}]
+R{"per_oper"}=? [ I=T {!"minimum"}{min} ]
 
 // from the inital state the expected time that the system is below minimum QOS until time T
-// (set OPERATIONAL to false, MINIMUM to 1 and REPAIR to false)
-R=?[C<=T ]
+R{"below_min"}=? [ C<=T ]
 
 // from the inital state the expected number of repairs by time T
-// (set OPERATIONAL to false, MINIMUM to 0 and REPAIR to true)
-R=?[C<=T ]
-
+R{"repairs"}=? [ C<=T ]
diff --git a/prism-examples/cluster/cluster.sm b/prism-examples/cluster/cluster.sm
index c38dba75..aeffe02d 100644
--- a/prism-examples/cluster/cluster.sm
+++ b/prism-examples/cluster/cluster.sm
@@ -1,7 +1,7 @@
 // workstation cluster [HHK00]
 // dxp/gxn 11/01/00
 
-stochastic
+ctmc
 
 const int N; // number of workstations in each cluster
 const int left_mx = N; // number of work stations in left cluster
@@ -85,20 +85,23 @@ module ToRight = Line[line=Toright,
 	                  repairLine=repairToRight ]
 endmodule
 
-// rewards - see cluster.csl for info
-const bool OPERATIONAL = true;
-const double MINIMUM = 0;
-const bool REPAIR = false;
-
-rewards
-	
-	OPERATIONAL  : 100*(left_n+right_n)/(2*N); // percentage of operational workstations stations
-	!minimum : MINIMUM; // time that the system is not delivering at least minimum QOS
-	// number of repairs
+// reward structures
+
+// percentage of operational workstations stations
+rewards "per_oper"
+	true : 100*(left_n+right_n)/(2*N);
+endrewards
+
+// time spent below minimum QoS
+rewards "below_min"
+	!minimum : 1;
+endrewards
+
+// number of repairs
+rewards "repairs"
 	[repairLeft]    REPAIR : 1;
 	[repairRight]   REPAIR : 1;
 	[repairToLeft]  REPAIR : 1;
 	[repairToRight] REPAIR : 1;
 	[repairLine]    REPAIR : 1;
-	
 endrewards