% t1 = 0.2; % t2 = 0.5; % t3 = 0.0333333333333333; % w1xr11 = 4; % w1xr12 = 2.4; % w1xr13 = 1.6; % w1xrr1 = 7; % w2xr21 = 1.2; % w2xr22 = 1.2; % w2xr23 = 0.6; % w2xrr2 = 9; % w3xr31 = 0.6; % w3xr32 = 0.6; % w3xr33 = 0.8; % w3xrr3 = 7; % rl11 = 8; % rl12 = 8; % rl13 = 8; % rl1r = 8; % rl21 = 8; % rl22 = 8; % rl23 = 8; % rl2r = 8; % rl31 = 8; % rl32 = 8; % rl33 = 8; % rl3r = 8; % e1 = 8; % e1f = 8; % r1 = 8; % e2 = 8; % e2f = 8; % r2 = 8; % e3 = 8; % e3f = 8; % r3 = 8; % a11xq = 10; % a11xonemq = 10; % a12xq = 20; % a12xonemq = 10; % a13xq = 10; % a13xonemq = 10; % a1rxq = 10; % a1rxonemq = 10; % a21xq = 13.3333333333333; % a21xonemq = 6.66666666666667; % a22xq = 13.3333333333333; % a22xonemq = 6.66666666666667; % a23xq = 13.3333333333333; % a23xonemq = 6.66666666666667; % a2rxq = 13.3333333333333; % a2rxonemq = 6.66666666666667; % a31xq = 16.6666666666667; % a31xonemq = 3.33333333333333; % a32xq = 16.6666666666667; % a32xonemq = 3.33333333333333; % a33xq = 16.6666666666667; % a33xonemq = 3.33333333333333; % a3rxq = 16.6666666666667; % a3rxonemq = 3.33333333333333; #txnc1 = (think1,t1).txn1; #txn1 = (fork, w1xr11).(reqlock11,rl11).(writelock11,infty).((finish,a11xq).txn1 + (finish,a11xonemq).txnc1) + (fork, w1xr12).(reqlock12,rl12).(writelock12,infty).((finish,a12xq).txn1 + (finish,a12xonemq).txnc1) + (fork, w1xrr1).(reqlock1r,rl1r).(readlock,r1).((finish,a1rxq).txn1 + (finish,a1rxonemq).txnc1); #lockmgr1 = (reqlock11, infty).lockmgr1_1 + (reqlock21, infty).lockmgr1_2; #lockmgr1_1 = (reqlock21, infty).lockmgr1_21 + (writelock11, e1).lockmgr1; #lockmgr1_2 = (reqlock11, infty).lockmgr1_12 + (writelock21, e1).lockmgr1; #lockmgr1_12 = (writelock21, e1).lockmgr1_1; #lockmgr1_21 = (writelock11, e1).lockmgr1_2; #lockmgr2 = (reqlock12, infty).lockmgr2_1 + (reqlock22, infty).lockmgr2_2; #lockmgr2_1 = (reqlock22, infty).lockmgr2_21 + (writelock12, e2).lockmgr2; #lockmgr2_2 = (reqlock12, infty).lockmgr2_12 + (writelock22, e2).lockmgr2; #lockmgr2_12 = (writelock22, e2).lockmgr2_1; #lockmgr2_21 = (writelock12, e2).lockmgr2_2; (txnc1) (lockmgr1 <> lockmgr2)