Commit d20027d6 authored by Ballarini Paolo's avatar Ballarini Paolo
Browse files

Replace 3M.prism

parent bf4edbca
dtmc
const double p1=1;//0.1; // fail probability of machine1
const double p2=0.1; // fail probability of machine2
const double p3=0.2; // fail probability of machine3
const double r1=0;//0.1; // repair probability of machine1
const double p1=0.01; // fail probability of machine1
const double p2=0.05; // fail probability of machine2
const double p3=0.02; // fail probability of machine3
const double r1=0.1; // repair probability of machine1
const double r2=0.2; // repair probability of machine2
const double r3=0.15; // repair probability of machine3
const int n0=2; // capacity of fictitious buffer zero is set to 2
const int n1=4; // capacity of buffer 1
const int n2=4; // capacity of buffer 2
const int n1=8; // capacity of buffer 1
const int n2=5; // capacity of buffer 2
const int n3=2; // capacity of fictitious last buffer is set to 2
const int m1init=1; // initial state of machine 1
const int m1init=8; // initial state of machine 1
const int m2init=1; // initial state of machine 2
const int m3init=1; // initial state of machine 3
const int b1init=2; // initial state of buffer 4
const int b2init=2; // initial state of buffer 5
formula totalpieces=(b1+b2);
const int m3init=0; // initial state of machine 3
const int b1init=1; // initial state of buffer 4
const int b2init=4; // initial state of buffer 5
module Phase
ph : [1..2] init 1;
......@@ -55,7 +53,44 @@ module B3
b3: [0..n3] init 1; // fictitious buffer with constant state (placeholder)
endmodule
// WIP (work in progress)
rewards "WIP"
true : b1+b2;
endrewards
// BUFFER OCCUPATION (num. of pieces in a buffer)
const int N;
rewards "B1level"
b1=N:1;
endrewards
rewards "B2level"
b2=N:1;
endrewards
// BLOCKING (buffer is full)
rewards "blocking1"
b1=n1:1;
endrewards
rewards "blocking2"
b2=n2:1;
endrewards
// STARVATION (buffer is empty)
rewards "starvation1"
b1=0:1;
endrewards
rewards "starvation2"
b2=0:1;
endrewards
// THROUGHPUT
rewards "throughput_M1"
[toc] ((m1=1 & b0>0 & b1<n1) & !(m2=1 & b1>0 & b2<n2)) | ((m1=1 & b0>0 & b1<n1) & (m2=1 & b1>0 & b2<n2)):1;
endrewards
rewards "throughput_M2"
[toc] ((m2=1 & b1>0 & b2<n2) & !(m3=1 & b2>0 & b3<n3)) | ((m2=1 & b1>0 & b2<n2) & (m3=1 & b2>0 & b3<n3)):1;
endrewards
rewards "throughput_M3"
[toc] ((m3=1 & b2>0 & b3<n3) & !(b3>0 )) | ((m3=1 & b2>0 & b3<n3) & (b3>0 )):1;
endrewards
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment