diff --git a/prism-examples/cluster/cluster.csl b/prism-examples/cluster/cluster.csl index a328296d..64486c97 100644 --- a/prism-examples/cluster/cluster.csl +++ b/prism-examples/cluster/cluster.csl @@ -1,45 +1,52 @@ -// properties from [HHK00] +// Properties based on those from [HHK00] -// left_operational_i : left_n>=i & Toleft_n -// right_operational_i : right_n>=i & Toright_n -// operational_i : (left_n+right_n)>=i & Toleft_n & line_n & Toright_n +// left_operational_i : left_n>=i & toleft_n +// right_operational_i : right_n>=i & toright_n +// 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 - -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); - +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 +// In the long run, the probability that premium QoS will be delivered S=? [ "premium" ] -// in the long run, the chance that QOS is below minimum +// In the long run, the chance that QoS is below minimum S=? [ !"minimum" ] -// the system will always be able to offer premium QOS at some point in the future +// The system will always be able to offer premium QoS at some point in the future P>=1 [ true U "premium" ] -// the chance that QOS drops below minimum quality within T time units (from the initial state) +// The chance that QoS drops below minimum quality within T time units +// (from the initial state) P=? [ true U<=T !"minimum" ] -// if facing insufficient QOS, the maximum probability of facing the same problem after T time units +// If facing insufficient QoS, the maximum probability of facing +// the same problem after T time units P=? [ true U[T,T] !"minimum" {!"minimum"}{max} ] -// the minimum probability of going from minimum QOS to premium QOS within T time units +// The minimum probability of going from minimum QoS to premium QoS +// within T time units 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 +// 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} ] -// the maximum probability that it takes more than T time units to recover from insufficient QOS +// 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 -R{"per_oper"}=? [ I=T {!"minimum"}{min} ] +// The minimum percentage of operational workstations at time T +// when starting from below minimum QoS +R{"percent_op"}=?[ I=T {!"minimum"}{min} ] + +// The expected time (from the initial state) +// that the system spends below minimum QoS until time T +R{"time_not_min"}=?[ C<=T ] -// from the inital state the expected time that the system is below minimum QOS until time T -R{"below_min"}=? [ C<=T ] +// The expected number of repairs by time T (starting in the initial state) +R{"num_repairs"}=?[ C<=T ] -// from the inital state the expected number of repairs by time T -R{"repairs"}=? [ C<=T ] diff --git a/prism-examples/cluster/cluster.sm b/prism-examples/cluster/cluster.sm index aeffe02d..e9e1bff8 100644 --- a/prism-examples/cluster/cluster.sm +++ b/prism-examples/cluster/cluster.sm @@ -1,107 +1,107 @@ -// workstation cluster [HHK00] +// Workstation cluster [HHK00] // dxp/gxn 11/01/00 ctmc -const int N; // number of workstations in each cluster -const int left_mx = N; // number of work stations in left cluster -const int right_mx = N; // number of work stations in right cluster +const int N; // Number of workstations in each cluster +const int left_mx = N; // Number of work stations in left cluster +const int right_mx = N; // Number of work stations in right cluster -// minimum QOS requires 3/4*N connected workstations operational -const int k=floor(0.75*N); -formula minimum = (left_n>=k & Toleft_n) | - (right_n>=k & Toright_n) | - ((left_n+right_n)>=k & Toleft_n & line_n & Toright_n); +// Minimum QoS requires 3/4 connected workstations operational +const int k = floor(0.75*N); +formula minimum = (left_n>=k & toleft_n) | + (right_n>=k & toright_n) | + ((left_n+right_n)>=k & toleft_n & line_n & toright_n); -// rates -const double line_rate = 0.0002; -const double Toleft_rate = 0.00025; -const double Toright_rate = 0.00025; +// Failure rates +const double ws_fail = 1/500; // Single workstation: average time to fail = 500 hrs +const double switch_fail = 1/4000; // Switch: average time to fail = 4000 hrs +const double line_fail = 1/5000; // Backbone: average time to fail = 5000 hrs -// left cluster +// Left cluster module Left - left_n : [0..left_mx] init left_mx; // number of workstations operational - left : bool; // being repaired? + left_n : [0..left_mx] init left_mx; // Number of workstations operational + left : bool; // Being repaired? [startLeft] !left & (left_n 1 : (left'=true); [repairLeft] left & (left_n 1 : (left'=false) & (left_n'=left_n+1); - [] (left_n>0) -> 0.002*left_n : (left_n'=left_n-1); + [] (left_n>0) -> ws_fail*left_n : (left_n'=left_n-1); endmodule -// right cluster +// Right cluster module Right = Left[left_n=right_n, - left=right, - left_mx=right_mx, - startLeft=startRight, - repairLeft=repairRight ] + left=right, + left_mx=right_mx, + startLeft=startRight, + repairLeft=repairRight ] endmodule -// repair unit +// Repair unit module Repairman - r : bool; // repairing? + r : bool; // Repairing? - [startLeft] !r -> 10 : (r'=true); // inspect Left - [startRight] !r -> 10 : (r'=true); // inspect Right - [startToLeft] !r -> 10 : (r'=true); // inspect ToLeft - [startToRight] !r -> 10 : (r'=true); // inspect ToRight - [startLine] !r -> 10 : (r'=true); // inspect Line + [startLeft] !r -> 10 : (r'=true); // Inspect Left + [startRight] !r -> 10 : (r'=true); // Inspect Right + [startToLeft] !r -> 10 : (r'=true); // Inspect ToLeft + [startToRight] !r -> 10 : (r'=true); // Inspect ToRight + [startLine] !r -> 10 : (r'=true); // Inspect Line - [repairLeft] r -> 2 : (r'=false); // repair Left - [repairRight] r -> 2 : (r'=false); // repair Right - [repairToLeft] r -> 0.25 : (r'=false); // repair ToLeft - [repairToRight] r -> 0.25 : (r'=false); // repair ToRight - [repairLine] r -> 0.125 : (r'=false); // repair Line + [repairLeft] r -> 2 : (r'=false); // Repair Left + [repairRight] r -> 2 : (r'=false); // Repair Right + [repairToLeft] r -> 0.25 : (r'=false); // Repair ToLeft + [repairToRight] r -> 0.25 : (r'=false); // Repair ToRight + [repairLine] r -> 0.125 : (r'=false); // Repair Line endmodule -// line/backbone +// Line/backbone module Line - line : bool; // being repaired? - line_n : bool init true; // working? + line : bool; // Being repaired? + line_n : bool init true; // Working? [startLine] !line & !line_n -> 1 : (line'=true); [repairLine] line & !line_n -> 1 : (line'=false) & (line_n'=true); - [] line_n -> line_rate : (line_n'=false); + [] line_n -> line_fail : (line_n'=false); endmodule -// left switch -module ToLeft = Line[line=Toleft, - line_n=Toleft_n, - line_rate=Toleft_rate, - startLine=startToLeft, - repairLine=repairToLeft ] +// Left switch +module ToLeft = Line[line=toleft, + line_n=toleft_n, + line_fail=switch_fail, + startLine=startToLeft, + repairLine=repairToLeft ] endmodule -// right switch -module ToRight = Line[line=Toright, - line_n=Toright_n, - line_rate=Toright_rate, - startLine=startToRight, - repairLine=repairToRight ] +// Right switch +module ToRight = Line[line=toright, + line_n=toright_n, + line_fail=switch_fail, + startLine=startToRight, + repairLine=repairToRight ] endmodule -// reward structures - -// percentage of operational workstations stations -rewards "per_oper" +// Reward structures + +// Percentage of operational workstations stations +rewards "percent_op" 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 + +// Time that the system is not delivering at least minimum QoS +rewards "time_not_min" + !minimum : 1; +endrewards + +// Number of repairs +rewards "num_repairs" + [repairLeft] true : 1; + [repairRight] true : 1; + [repairToLeft] true : 1; + [repairToRight] true : 1; + [repairLine] true : 1; endrewards