Upload New File

2_slot_models/3M.props

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