Browse Source
Moved labels to model in cluster.
Moved labels to model in cluster.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1845 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
16 years ago
2 changed files with 160 additions and 159 deletions
@ -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 ] |
|||
|
|||
@ -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<left_mx) -> 1 : (left'=true); |
|||
[repairLeft] left & (left_n<left_mx) -> 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<left_mx) -> 1 : (left'=true); |
|||
[repairLeft] left & (left_n<left_mx) -> 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 |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue