From 02c952a1b5cc2efeaa0769f89996bdac6a8a858b Mon Sep 17 00:00:00 2001
From: Gethin Norman <gethin.norman@glasgow.ac.uk>
Date: Wed, 21 Nov 2007 15:18:02 +0000
Subject: [PATCH] added reward structures for fms

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@527 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism-examples/fms/fms.csl | 10 +++++++++-
 prism-examples/fms/fms.sm  | 38 +++++++++++++++++++++++++-------------
 2 files changed, 34 insertions(+), 14 deletions(-)

diff --git a/prism-examples/fms/fms.csl b/prism-examples/fms/fms.csl
index eed570f5..d62fcf54 100644
--- a/prism-examples/fms/fms.csl
+++ b/prism-examples/fms/fms.csl
@@ -1 +1,9 @@
-R=? [ S ]
+// expected throughput of each machine
+R{"throughput_m1"}=?  [ S ]
+R{"throughput_m2"}=?  [ S ]
+R{"throughput_m3"}=?  [ S ]
+R{"throughput_m12"}=? [ S ]
+
+// expected productivity of the system
+R{"productivity"}=? [ S ]
+
diff --git a/prism-examples/fms/fms.sm b/prism-examples/fms/fms.sm
index 24a2dec4..318a4a3a 100644
--- a/prism-examples/fms/fms.sm
+++ b/prism-examples/fms/fms.sm
@@ -1,14 +1,13 @@
 // flexible manufacturing system [CT93]
 // gxn/dxp 11/06/01
 
-stochastic
-
-// number of tokens
-const int n;
+ctmc // model is a ctmc
+
+const int n; // number of tokens
 
 // rates from Pi equal #(Pi) * min(1, np/r)
 // where np = (3n)/2 and r = P1+P2+P3+P12
-const int np=floor((3*n)/2); // np = 3n/2
+const int np=floor((3*n)/2);
 formula r = P1+P2+P3+P12;
 
 module machine1
@@ -99,16 +98,29 @@ module machine12
 	[fp12] (P12s>0) -> 1/60 : (P12s'=0);
 	
 endmodule
-
-rewards
-	
-// 	[t1]  true : 1;
-// 	[t2]  true : 1;
-// 	[t3]  true : 1;
-// 	[t12] true : 1;
+
+// reward structures
+
+// throughput of machine1
+rewards "throughput_m1"
+	[t1]  true : 1;	
+endrewards
+// throughput of machine2
+rewards "throughput_m2"
+	[t2]  true : 1;	
+endrewards
+// throughput of machine3
+rewards "throughput_m3"
+	[t3]  true : 1;	
+endrewards
+// throughput of machine12
+rewards "throughput_m12"
+	[t12]  true : 1;	
+endrewards
+// productivity of the system
+rewards "productivity"
 	[t1]  true : 400;
 	[t2]  true : 600;
 	[t3]  true : 100;
 	[t12] true : 1100;
-	
 endrewards