Commit 9239101b authored by Ballarini Paolo's avatar Ballarini Paolo
Browse files

Upload New File

parent c523ee6d
const int T; // time bound constant
// safety check1: a machine cannot be broken and its downstream buffer full
"safe1": P=? [ F(((m1=0) & (b1=n1))|((m2=0) & (b2=n2))|((m3=0) & (b3=n3)))]
// safety check2 : full adjacent buffers cannot become both non-full in one time unit
"safe2_b1": (b1=n1 & b2=n2) => P<=0[X(b1<n1 & b2<n2)]
"safe2_b2": (b2=n2 & b3=n3) => P<=0[X(b2<n2 & b3<n3)]
"safe2_AllBuffers": ((b1=n1 & b2=n2) => P<=0[X(b1<n1 & b2<n2)]) & ((b2=n2 & b3=n3) => P<=0[X(b2<n2 & b3<n3)])
// Probability first N buffers gets full within time T
"full_first_1_buffers": P=? [ F<=T(b1=n1)]
"full_first_2_buffers": P=? [ F<=T(b1=n1 & b2=n2)]
"full_first_3_buffers": P=? [ F<=T(b1=n1 & b2=n2 & b3=n3)]
// Reward-based formulae
R{"WIP"}=? [ S ]
R{"B1level"}=? [ S ]
R{"B2level"}=? [ S ]
R{"B3level"}=? [ S ]
R{"blocking1"}=? [ S ]
R{"blocking1"}=? [ I=T ]
R{"blocking2"}=? [ S ]
R{"blocking2"}=? [ I=T ]
R{"blocking3"}=? [ S ]
R{"blocking3"}=? [ I=T ]
R{"starvation1"}=? [ S ]
R{"starvation1"}=? [ I=T ]
R{"starvation2"}=? [ S ]
R{"starvation2"}=? [ I=T ]
R{"starvation3"}=? [ S ]
R{"starvation3"}=? [ I=T ]
R{"throughput_M1"}=? [ S ]
R{"throughput_M2"}=? [ S ]
R{"throughput_M3"}=? [ S ]
R{"throughput_M4"}=? [ S ]
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