From ac7060c92d974e2de53e15be8444398936be3ba0 Mon Sep 17 00:00:00 2001
From: Gethin Norman <gethin.norman@glasgow.ac.uk>
Date: Mon, 26 Nov 2007 11:25:41 +0000
Subject: [PATCH] various fixes to update rewards and match web pages

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@535 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism-examples/cell/cell.csl         | 23 +++++++++++++--------
 prism-examples/embedded/embedded.csl | 30 +++++++++++++++++----------
 prism-examples/embedded/embedded.sm  | 25 +++++++++++++---------
 prism-examples/kanban/auto           |  2 +-
 prism-examples/kanban/kanban.csl     |  9 +++++++-
 prism-examples/kanban/kanban.sm      | 31 +++++++++++++++++++++++-----
 6 files changed, 83 insertions(+), 37 deletions(-)

diff --git a/prism-examples/cell/cell.csl b/prism-examples/cell/cell.csl
index f7ea40a4..13b54bc9 100644
--- a/prism-examples/cell/cell.csl
+++ b/prism-examples/cell/cell.csl
@@ -1,16 +1,21 @@
-const double T;
+const double T; // time bound
 
-// what is the maximum probability that a hand off call can be dropped within t time units (assuming a guarded channel is free)
+// the maximum probability that a hand off call can be dropped within t time units (assuming a guarded channel is free)
 P=?[ true U<=T (n=N) {n<N}{max} ]
-// what is the maximum probability that a call can be dropped within t time units (assuming a non-guarded channel is free)
+
+// the maximum probability that a call can be dropped within t time units (assuming a non-guarded channel is free)
 P=?[ true U<=T (n>=N*0.8) {n<N*0.8}{max} ]
-// what is the minimum probability that a cell will be accepted within T time units (assuming no channels are free)
+
+// the minimum probability that a cell will be accepted within T time units (assuming no channels are free)
 P=?[ true U<=T (n<N*0.8) {n=N}{min} ]
-// what is the expected number of calls at time T
-R=? [ I=T ]
-// what is the probability that in the long run any call can be dropped
+
+// the expected number of calls at time T
+R{"calls"}=? [ I=T ]
+
+// the probability that in the long run any call can be dropped
 S=? [ n<N*0.8 ]
-// what is the probability that in the long run a hand-off call can be dropped
-R=? [ S ]
+
+// the expected number calls in the cell in the long run
+R{"calls"}=? [ S ]
 
 
diff --git a/prism-examples/embedded/embedded.csl b/prism-examples/embedded/embedded.csl
index ca927fea..d3892581 100644
--- a/prism-examples/embedded/embedded.csl
+++ b/prism-examples/embedded/embedded.csl
@@ -1,10 +1,15 @@
-const double T;
-
-label "fail_sensors" = i=2&s<MIN_SENSORS;
-label "fail_actuators" = o=2&a<MIN_ACTUATORS;
-label "fail_io" = count=MAX_COUNT+1;
-label "fail_main" = m=0;
-label "down" = (i=2&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0);
+const double T; // time bound
+
+// causes of failues
+label "fail_sensors" = i=2&s<MIN_SENSORS; // sensors have failed
+label "fail_actuators" = o=2&a<MIN_ACTUATORS; // actuators have failed
+label "fail_io" = count=MAX_COUNT+1; // IO has failed
+label "fail_main" = m=0; // ,main processor has failed
+
+// system status
+label "down" = (i=2&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0); // system has shutdown
+label "danger" = !down & (i=1 | o=1); // transient fault has occured
+label "up" = !down & !danger; // system is operational
 
 // Probability of any failure occurring within T hours
 P=? [ true U<=T*3600 "down" ]
@@ -30,8 +35,11 @@ P=? [ !"down" U "fail_actuators" ]
 P=? [ !"down" U "fail_io" ]
 P=? [ !"down" U "fail_main" ]
 
-// Expected time spent in "up"/"danger"/"shutdown" by time T
-R=? [ C<=T*3600 ]
+// Expected time spent in "up"/"danger"/"down" by time T
+R{"up"}=? [ C<=T*3600 ]
+R{"danger"}=? [ C<=T*3600 ]
+R{"down"}=? [ C<=T*3600 ]
 
-// Expected time spent in "up"/"danger" before "shutdown"
-R=? [ F "down" ]
+// Expected time spent in "up"/"danger" before "down"
+R{"up"}=? [ F "down" ]
+R{"danger"}=? [ F "down" ]
diff --git a/prism-examples/embedded/embedded.sm b/prism-examples/embedded/embedded.sm
index 3010dc40..0208248a 100644
--- a/prism-examples/embedded/embedded.sm
+++ b/prism-examples/embedded/embedded.sm
@@ -115,17 +115,22 @@ module bus
 	& (reqo'=!(o=2 & a>=1) & (reqo | (reqi & m=1)));
 	
 endmodule
-
-formula fail_sensors = i=2&s<MIN_SENSORS;
-formula fail_actuators = o=2&a<MIN_ACTUATORS;
-formula fail_io = count=MAX_COUNT+1;
-formula fail_main = m=0;
-formula down = (i=2&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0);
-formula danger = !down & (i=1 | o=1);
+
+// the system is down
+formula down = (i=2&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0);
+// transient failure has occured but the system is not down
+formula danger = !down & (i=1 | o=1);
+// the system is operational
 formula up = !down & !danger;
+
+// reward structures
 
-rewards
+rewards "up"
 	up : 1/3600;
-// 	danger : 1/3600;
-// 	down : 1/3600;
+endrewards
+
rewards "danger"
+	danger : 1/3600;
 endrewards
+rewards "down"
+	down : 1/3600;
+endrewards
diff --git a/prism-examples/kanban/auto b/prism-examples/kanban/auto
index df9f14b5..93b159d9 100755
--- a/prism-examples/kanban/auto
+++ b/prism-examples/kanban/auto
@@ -1,5 +1,5 @@
 #!/bin/csh
 
 foreach t (1 2 3 4 5 6 7 8)
-	prism kanban.sm kanban.csl -const t=$t -sor
+	prism kanban.sm kanban.csl -const t=$t -jor
 end
diff --git a/prism-examples/kanban/kanban.csl b/prism-examples/kanban/kanban.csl
index eed570f5..5217fc96 100644
--- a/prism-examples/kanban/kanban.csl
+++ b/prism-examples/kanban/kanban.csl
@@ -1 +1,8 @@
-R=? [ S ]
+// expected number of tokens in each cell
+R{"tokens_cell1"}=? [ S ]
+R{"tokens_cell2"}=? [ S ]
+R{"tokens_cell3"}=? [ S ]
+R{"tokens_cell4"}=? [ S ]
+
+// expected throughput of the system
+R{"throughput"}=? [ S ]
diff --git a/prism-examples/kanban/kanban.sm b/prism-examples/kanban/kanban.sm
index ab0f64ea..8f50e410 100644
--- a/prism-examples/kanban/kanban.sm
+++ b/prism-examples/kanban/kanban.sm
@@ -6,7 +6,7 @@ stochastic
 // number of tokens 
 const int t; 
 
-// const doubles
+// rates
 const double in1      = 1.0;
 const double out4     = 0.9;
 const double synch123 = 0.4;
@@ -81,10 +81,31 @@ module k4
 	[]   (z4>0) & (w4>0) -> out4 	: (z4'=z4-1) & (w4'=w4-1);
 
 endmodule
-
-rewards
-	
+
+// reward structures
+
+// tokens in cell1
+rewards "tokens_cell1"
+	true : x1+y1+z1;
+endrewards
+
+// tokens in cell2
+rewards "tokens_cell2"
+	true : x2+y2+z2;
+endrewards
+
+// tokens in cell3
+rewards "tokens_cell3"
+	true : x3+y3+z3;
+endrewards
+
+// tokens in cell4
+rewards "tokens_cell4"
+	true : x4+y4+z4;
+endrewards
+
+// throughput of the system
+rewards "throughput"
 	[in] true : 1;
-	
 endrewards