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)))]

// 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_AllBuffers": ((b1=n1 & b2=n2) => P<=0[X(b1<n1 & b2<n2)])

// 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)]


// Reward-based formulae
R{"WIP"}=? [ S ] 

R{"B1level"}=? [ S ] 
R{"B2level"}=? [ S ] 

R{"blocking1"}=? [ S ] 
R{"blocking1"}=? [ I=T ] 
R{"blocking2"}=? [ S ] 
R{"blocking2"}=? [ I=T ] 

R{"starvation1"}=? [ S ] 
R{"starvation1"}=? [ I=T ] 
R{"starvation2"}=? [ S ] 
R{"starvation2"}=? [ I=T ] 

R{"throughput_M1"}=? [ S ] 
R{"throughput_M2"}=? [ S ] 
R{"throughput_M3"}=? [ S ]