From fa3b003c4cb69b4d1ee43dd53750a576aa4dfc20 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 23 Apr 2010 08:23:40 +0000 Subject: [PATCH] Moved labels to model in cluster. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1845 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/cluster/cluster.csl | 96 ++++++------- prism-examples/cluster/cluster.sm | 223 +++++++++++++++-------------- 2 files changed, 160 insertions(+), 159 deletions(-) diff --git a/prism-examples/cluster/cluster.csl b/prism-examples/cluster/cluster.csl index 64486c97..aeb77792 100644 --- a/prism-examples/cluster/cluster.csl +++ b/prism-examples/cluster/cluster.csl @@ -1,52 +1,44 @@ -// 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 -// 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); - -const double T; - -// 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 -S=? [ !"minimum" ] - -// 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) -P=? [ true U<=T !"minimum" ] - -// 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 -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} ] - -// The maximum probability that it takes more than T time units -// to recover from insufficient QoS -P=? [ !"minimum" U>=T "minimum" {!"minimum"}{max} ] - -// 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 ] - -// The expected number of repairs by time T (starting in the initial state) -R{"num_repairs"}=?[ C<=T ] - +// Properties based on those from [HHK00] + +const double T; + +// 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 +S=? [ !"minimum" ] + +// 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) +P=? [ true U<=T !"minimum" ] + +// 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 +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} ] + +// The maximum probability that it takes more than T time units +// to recover from insufficient QoS +P=? [ !"minimum" U>=T "minimum" {!"minimum"}{max} ] + +// 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 ] + +// The expected number of repairs by time T (starting in the initial state) +R{"num_repairs"}=?[ C<=T ] + diff --git a/prism-examples/cluster/cluster.sm b/prism-examples/cluster/cluster.sm index e9e1bff8..a4835120 100644 --- a/prism-examples/cluster/cluster.sm +++ b/prism-examples/cluster/cluster.sm @@ -1,107 +1,116 @@ -// 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 - -// 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); - -// 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 -module Left - - 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) -> ws_fail*left_n : (left_n'=left_n-1); - -endmodule - -// Right cluster -module Right = Left[left_n=right_n, - left=right, - left_mx=right_mx, - startLeft=startRight, - repairLeft=repairRight ] -endmodule - -// Repair unit -module Repairman - - 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 - - [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 -module Line - - 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_fail : (line_n'=false); - -endmodule - -// 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_fail=switch_fail, - startLine=startToRight, - repairLine=repairToRight ] -endmodule - -// Reward structures - -// Percentage of operational workstations stations -rewards "percent_op" - true : 100*(left_n+right_n)/(2*N); -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 +// 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 + +// 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 +module Left + + 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) -> ws_fail*left_n : (left_n'=left_n-1); + +endmodule + +// Right cluster +module Right = Left[left_n=right_n, + left=right, + left_mx=right_mx, + startLeft=startRight, + repairLeft=repairRight ] +endmodule + +// Repair unit +module Repairman + + 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 + + [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 +module Line + + 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_fail : (line_n'=false); + +endmodule + +// 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_fail=switch_fail, + startLine=startToRight, + repairLine=repairToRight ] +endmodule + +// Formulas + labels + +// Minimum QoS requires 3/4 connected workstations operational +const int k = floor(0.75*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 +formula minimum = (left_n>=k & toleft_n) | + (right_n>=k & toright_n) | + ((left_n+right_n)>=k & 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); +// premium = minimum_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); + +// Reward structures + +// Percentage of operational workstations stations +rewards "percent_op" + true : 100*(left_n+right_n)/(2*N); +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