Upload New File

2_slot_models/7M.prism

+dtmc
+
+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 p4=0.03;  // fail probability of machine4 
+const double p5=0.01;  // fail probability of machine5 
+const double p6=0.05;  // fail probability of machine6 
+const double p7=0.02;  // fail probability of machine7 
+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 double r4=0.18;  // repair probability of machine4 
+const double r5=0.1;  // repair probability of machine5 
+const double r6=0.2;  // repair probability of machine6 
+const double r7=0.15;  // repair probability of machine7 
+const int n0=2;  // capacity of fictitious buffer zero is set to 2 
+const int n1=8;  // capacity of buffer 1 
+const int n2=5;  // capacity of buffer 2 
+const int n3=8;  // capacity of buffer 3 
+const int n4=8;  // capacity of buffer 4 
+const int n5=5;  // capacity of buffer 5 
+const int n6=8;  // capacity of buffer 6 
+const int n7=2;  // capacity of fictitious last buffer is set to 2 
+const int m1init=1;  // initial state of machine 1 
+const int m2init=0;  // initial state of machine 2 
+const int m3init=1;  // initial state of machine 3 
+const int m4init=1;  // initial state of machine 4 
+const int m5init=1;  // initial state of machine 5 
+const int m6init=0;  // initial state of machine 6 
+const int m7init=1;  // initial state of machine 7 
+const int b1init=4;  // initial state of buffer 8 
+const int b2init=2;  // initial state of buffer 9 
+const int b3init=7;  // initial state of buffer 10 
+const int b4init=4;  // initial state of buffer 11 
+const int b5init=2;  // initial state of buffer 12 
+const int b6init=7;  // initial state of buffer 13 
+
+module Phase
+ph : [1..2] init 1;
+[tic] ph=1 -> 1:(ph'=2);
+[toc] ph=2 -> 1:(ph'=1);
+endmodule
+
+module B0
+  b0 : [0..n0] init 1; // fictitious buffer with constant state (placeholder)
+endmodule
+
+module M1 // intermediate machine, b0: upstream buffer, b1: downstream buffer
+  m1 : [0..1] init m1init;
+ 
+  [tic] m1=1   -> p1:(m1' =  (b1=n1 | b0=0) ? 1 : 0) + (1-p1):(m1'=1);
+  [toc] true -> 1:true;
+  [tic] m1=0   -> r1:(m1'=1) + (1-r1):(m1'=0);  
+endmodule
+
+module B1 // intermediate buffer, m1: upstream machine, m2: downstream machine, 
+          //                      b0: upstream buffer, b2: downstream buffer
+  b1 : [0..n1] init b1init; 
+
+  [tic] true -> 1:true;
+  [toc] ((m1=1 & b0>0 & b1<n1) & !(m2=1 & b1>0 & b2<n2)) -> 1:(b1'=b1+1); // increase buffer occupation
+  [toc] (!(m1=1 & b0>0 & b1<n1) & (m2=1 & b1>0 & b2<n2)) -> 1:(b1'=b1-1); // decrease buffer occupation
+  [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:(b1'=b1); // buffer unchanged
+endmodule
+
+module M2= M1[m1=m2, b0=b1, b1=b2, p1=p2, r1=r2, n1=n2, m1init=m2init] endmodule 
+module B2= B1[b1=b2, m1=m2, m2=m3, b0=b1, b2=b3, n1=n2, n2=n3, b1init=b2init] endmodule 
+module M3= M2[m2=m3, b1=b2, b2=b3, p2=p3, r2=r3, n2=n3, m2init=m3init] endmodule 
+module B3= B2[b2=b3, m2=m3, m3=m4, b1=b2, b3=b4, n2=n3, n3=n4, b2init=b3init] endmodule 
+module M4= M3[m3=m4, b2=b3, b3=b4, p3=p4, r3=r4, n3=n4, m3init=m4init] endmodule 
+module B4= B3[b3=b4, m3=m4, m4=m5, b2=b3, b4=b5, n3=n4, n4=n5, b3init=b4init] endmodule 
+module M5= M4[m4=m5, b3=b4, b4=b5, p4=p5, r4=r5, n4=n5, m4init=m5init] endmodule 
+module B5= B4[b4=b5, m4=m5, m5=m6, b3=b4, b5=b6, n4=n5, n5=n6, b4init=b5init] endmodule 
+module M6= M5[m5=m6, b4=b5, b5=b6, p5=p6, r5=r6, n5=n6, m5init=m6init] endmodule 
+module B6= B5[b5=b6, m5=m6, m6=m7, b4=b5, b6=b7, n5=n6, n6=n7, b5init=b6init] endmodule 
+module M7= M6[m6=m7, b5=b6, b6=b7, p6=p7, r6=r7, n6=n7, m6init=m7init] endmodule 
+
+module B7
+  b7: [0..n7] init 1; // fictitious buffer with constant state (placeholder)
+endmodule
+
+// WIP (work in progress)
+rewards "WIP"
+    true : b1+b2+b3+b4+b5+b6;
+endrewards
+
+// BUFFER OCCUPATION (num. of pieces in a buffer) 
+const int N;
+rewards "B1level"
+  b1=N:1;
+endrewards
+rewards "B2level"
+  b2=N:1;
+endrewards
+rewards "B3level"
+  b3=N:1;
+endrewards
+rewards "B4level"
+  b4=N:1;
+endrewards
+rewards "B5level"
+  b5=N:1;
+endrewards
+rewards "B6level"
+  b6=N:1;
+endrewards
+
+// BLOCKING (buffer is full) 
+rewards "blocking1"
+  b1=n1:1;
+endrewards
+rewards "blocking2"
+  b2=n2:1;
+endrewards
+rewards "blocking3"
+  b3=n3:1;
+endrewards
+rewards "blocking4"
+  b4=n4:1;
+endrewards
+rewards "blocking5"
+  b5=n5:1;
+endrewards
+rewards "blocking6"
+  b6=n6:1;
+endrewards
+
+// STARVATION (buffer is empty) 
+rewards "starvation1"
+  b1=0:1;
+endrewards
+rewards "starvation2"
+  b2=0:1;
+endrewards
+rewards "starvation3"
+  b3=0:1;
+endrewards
+rewards "starvation4"
+  b4=0:1;
+endrewards
+rewards "starvation5"
+  b5=0:1;
+endrewards
+rewards "starvation6"
+  b6=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) & !(m4=1 & b3>0 & b4<n4)) | ((m3=1 & b2>0 & b3<n3) & (m4=1 & b3>0 & b4<n4)):1;
+endrewards
+rewards "throughput_M4"
+[toc]  ((m4=1 & b3>0 & b4<n4) & !(m5=1 & b4>0 & b5<n5)) | ((m4=1 & b3>0 & b4<n4) & (m5=1 & b4>0 & b5<n5)):1;
+endrewards
+rewards "throughput_M5"
+[toc]  ((m5=1 & b4>0 & b5<n5) & !(m6=1 & b5>0 & b6<n6)) | ((m5=1 & b4>0 & b5<n5) & (m6=1 & b5>0 & b6<n6)):1;
+endrewards
+rewards "throughput_M6"
+[toc]  ((m6=1 & b5>0 & b6<n6) & !(m7=1 & b6>0 & b7<n7)) | ((m6=1 & b5>0 & b6<n6) & (m7=1 & b6>0 & b7<n7)):1;
+endrewards
+rewards "throughput_M7"
+[toc]  ((m7=1 & b6>0 & b7<n7) & !(b7>0 )) | ((m7=1 & b6>0 & b7<n7) & (b7>0 )):1;
+endrewards
+