s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Updates to cluster example. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@280 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 19 years ago
parent
2b134243c5
commit
de462f07c3
2 changed files with 97 additions and 90 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 51
      prism-examples/cluster/cluster.csl
  2. 136
      prism-examples/cluster/cluster.sm

51
prism-examples/cluster/cluster.csl
View File

@ -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 // minimum_k : left_operational_k | right_operational_k | operational_k
// premium = minimum_N // 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; 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" ] 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" ] 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" ] 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" ] 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} ] 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} ] 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} ] 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} ] 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 ]

136
prism-examples/cluster/cluster.sm
View File

@ -1,107 +1,107 @@
// workstation cluster [HHK00]
// Workstation cluster [HHK00]
// dxp/gxn 11/01/00 // dxp/gxn 11/01/00
ctmc 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 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<left_mx) -> 1 : (left'=true); [startLeft] !left & (left_n<left_mx) -> 1 : (left'=true);
[repairLeft] left & (left_n<left_mx) -> 1 : (left'=false) & (left_n'=left_n+1); [repairLeft] left & (left_n<left_mx) -> 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 endmodule
// right cluster
// Right cluster
module Right = Left[left_n=right_n, 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 endmodule
// repair unit
// Repair unit
module Repairman 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 endmodule
// line/backbone
// Line/backbone
module Line 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); [startLine] !line & !line_n -> 1 : (line'=true);
[repairLine] line & !line_n -> 1 : (line'=false) & (line_n'=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 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 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 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); 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 endrewards
Write Preview
Loading…
Cancel
Save