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

Replace 4M.prism

parent d1514867
......@@ -60,3 +60,56 @@ module B4
b4: [0..n4] init 1; // fictitious buffer with constant state (placeholder)
endmodule
// WIP (work in progress)
rewards "WIP"
true : b1+b2+b3;
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
// BLOCKING (buffer is full)
rewards "blocking1"
b1=n1:1;
endrewards
rewards "blocking2"
b2=n2:1;
endrewards
rewards "blocking3"
b3=n3:1;
endrewards
// STARVATION (buffer is empty)
rewards "starvation1"
b1=0:1;
endrewards
rewards "starvation2"
b2=0:1;
endrewards
rewards "starvation3"
b3=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) & !(b4>0 )) | ((m4=1 & b3>0 & b4<n4) & (b4>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