Commit 99ac72e3 authored by Ballarini Paolo's avatar Ballarini Paolo
Browse files

Adding PRISM DTMC model of type 2-slot for 3-machines production line

parent d7b95178
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 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 n3=2; // capacity of fictitious last buffer is set to 2
const int m1init=1; // 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);
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
b3: [0..n3] init 1; // fictitious buffer with constant state (placeholder)
endmodule
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