###keys
nw tran #req[1] #req[2] #req[3] pc[1] pc[2] pc[3] requesting[1] requesting[2] requesting[3] havePriv[1] havePriv[2] havePriv[3] rn[1] rn[2] rn[3] ln[1] ln[2] ln[3] queue[1] queue[2] queue[3] idx[1] idx[2] idx[3]

###textDisplay
###conditionDisplay
ln queue
ln[1] ln[2] ln[3] ****priv(_,ln)
ln[1]++++havePriv[1]==true
ln[2]++++havePriv[2]==true
ln[3]++++havePriv[3]==true
****priv(_,ln)++++nw
queue[1] queue[2] queue[3] ****priv(queue,_)
queue[1]++++havePriv[1]==true
queue[2]++++havePriv[2]==true
queue[3]++++havePriv[3]==true
****priv(queue,_)++++nw

###states
(nw: void tran: notran (#req[1]: 0) (#req[2]: 0) (#req[3]: 0) (pc[1]: rem) (pc[2]: rem) (pc[3]: rem) (requesting[1]: false) (requesting[2]: false) (requesting[3]: false) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: ia) (rn[3]: ia) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 1) || 
(nw: void tran: try(1) (#req[1]: 1) (#req[2]: 0) (#req[3]: 0) (pc[1]: l1) (pc[2]: rem) (pc[3]: rem) (requesting[1]: false) (requesting[2]: false) (requesting[3]: false) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: ia) (rn[3]: ia) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 1) || 
(nw: void tran: try(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 0) (pc[1]: l1) (pc[2]: l1) (pc[3]: rem) (requesting[1]: false) (requesting[2]: false) (requesting[3]: false) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: ia) (rn[3]: ia) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 1) || 
(nw: void tran: try(3) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l1) (pc[3]: l1) (requesting[1]: false) (requesting[2]: false) (requesting[3]: false) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: ia) (rn[3]: ia) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 1) || 
(nw: void tran: setReq(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l2) (pc[3]: l1) (requesting[1]: false) (requesting[2]: true) (requesting[3]: false) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: ia) (rn[3]: ia) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 1) || 
(nw: void tran: setReq(3) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l2) (pc[3]: l2) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: ia) (rn[3]: ia) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 1) || 
(nw: void tran: checkPriv(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l3) (pc[3]: l2) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: ia) (rn[3]: ia) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 1) || 
(nw: void tran: checkPriv(3) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l3) (pc[3]: l3) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: ia) (rn[3]: ia) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 1) || 
(nw: void tran: incReqNo(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l4) (pc[3]: l3) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: 2 : 1) (rn[3]: ia) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 1) || 
(nw: void tran: incReqNo(3) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l4) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 1) || 
(nw: msg(1, req(2, 1)) tran: sendReq(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l4) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 1) || 
(nw: (msg(1, req(2, 1)) ; msg(1, req(3, 1))) tran: sendReq(3) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l4) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 2) || 
(nw: (msg(1, req(2, 1)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1))) tran: sendReq(3) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l4) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: ia) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(2, priv(empty, ia))) tran: receiveReq(1) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l1) (pc[2]: l4) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: 2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(2, priv(empty, ia))) tran: setReq(1) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l2) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: 2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(2, priv(empty, ia))) tran: checkPriv(1) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l3) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: 2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(2, priv(empty, ia))) tran: incReqNo(1) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l4) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(2, priv(empty, ia))) tran: sendReq(1) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l4) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 2) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(2, priv(empty, ia))) tran: sendReq(1) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l4) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 3) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(2, priv(empty, ia))) tran: sendReq(1) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(2, priv(empty, ia))) tran: sendReq(1) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(2, priv(empty, ia))) tran: sendReq(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(2, priv(empty, ia))) tran: sendReq(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1))) tran: waitPriv(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: cs) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1))) tran: exit(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: l6) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: ia) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1))) tran: completeReq(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1))) tran: updateQueue(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1))) tran: updateQueue(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1))) tran: updateQueue(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: l8) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1))) tran: checkQueue(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: l10) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1))) tran: resetReq(2) (#req[1]: 1) (#req[2]: 1) (#req[3]: 1) (pc[1]: l5) (pc[2]: rem) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1))) tran: try(2) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l1) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: 2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(1, priv(empty, 2 : 1))) tran: receiveReq(2) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l1) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(1, priv(empty, 2 : 1))) tran: setReq(2) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l2) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(1, priv(empty, 2 : 1))) tran: checkPriv(2) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l3) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 1) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(1, priv(empty, 2 : 1))) tran: incReqNo(2) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(1, priv(empty, 2 : 1)))tran: sendReq(2) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(1, priv(empty, 2 : 1)))tran: sendReq(2) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(1, priv(empty, 2 : 1))) tran: sendReq(2) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(1, priv(empty, 2 : 1))) tran: sendReq(2) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: ia) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: waitPriv(1) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: cs) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: 2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: exit(1) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l6) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: 2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: completeReq(1) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: updateQueue(1) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 2) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: updateQueue(1) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 3) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: updateQueue(1) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l8) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: checkQueue(1) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: l10) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: resetReq(1) (#req[1]: 1) (#req[2]: 2) (#req[3]: 1) (pc[1]: rem) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 2)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: try(1) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l1) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 1) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(2, priv(empty, (1 : 1),2 : 1))) tran: receiveReq(1) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l1) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(2, priv(empty, (1 : 1),2 : 1))) tran: setReq(1) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l2) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(2, priv(empty, (1 : 1),2 : 1))) tran: checkPriv(1) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l3) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 1),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(2, priv(empty, (1 : 1),2 : 1))) tran: incReqNo(1) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(2, priv(empty, (1 : 1),2 : 1))) tran: sendReq(1) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 2) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(2, priv(empty, (1 : 1),2 : 1))) tran: sendReq(1) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 3) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(2, priv(empty, (1 : 1),2 : 1))) tran: sendReq(1) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(2, priv(empty, (1 : 1),2 : 1))) tran: sendReq(1) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: 2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: waitPriv(2) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: cs) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: exit(2) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l6) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 1) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: completeReq(2) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: updateQueue(2) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: updateQueue(2) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: updateQueue(2) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l8) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: checkQueue(2) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: l10) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: resetReq(2) (#req[1]: 2) (#req[2]: 2) (#req[3]: 1) (pc[1]: l5) (pc[2]: rem) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 2)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2))) tran: try(2) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l1) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 1),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(1, priv(empty, (1 : 1),2 : 2))) tran: receiveReq(2) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l1) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(1, priv(empty, (1 : 1),2 : 2))) tran: setReq(2) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l2) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(1, priv(empty, (1 : 1),2 : 2))) tran: checkPriv(2) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l3) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 2) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(1, priv(empty, (1 : 1),2 : 2))) tran: incReqNo(2) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(1, priv(empty, (1 : 1),2 : 2))) tran: sendReq(2) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(1, priv(empty, (1 : 1),2 : 2))) tran: sendReq(2) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(1, priv(empty, (1 : 1),2 : 2))) tran: sendReq(2) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(1, priv(empty, (1 : 1),2 : 2))) tran: sendReq(2) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 1) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: waitPriv(1) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: cs) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: exit(1) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l6) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 1),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: completeReq(1) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: updateQueue(1) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 2) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: updateQueue(1) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 3) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: updateQueue(1) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l8) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: checkQueue(1) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: l10) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: resetReq(1) (#req[1]: 2) (#req[2]: 3) (#req[3]: 1) (pc[1]: rem) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 3)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: try(1) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l1) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 2) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(2, priv(empty, (1 : 2),2 : 2))) tran: receiveReq(1) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l1) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(2, priv(empty, (1 : 2),2 : 2))) tran: setReq(1) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l2) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(2, priv(empty, (1 : 2),2 : 2))) tran: checkPriv(1) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l3) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 2),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(2, priv(empty, (1 : 2),2 : 2))) tran: incReqNo(1) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(2, priv(empty, (1 : 2),2 : 2))) tran: sendReq(1) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 2) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(2, priv(empty, (1 : 2),2 : 2))) tran: sendReq(1) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 3) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(2, priv(empty, (1 : 2),2 : 2))) tran: sendReq(1) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(2, priv(empty, (1 : 2),2 : 2))) tran: sendReq(1) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 1),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: waitPriv(2) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: cs) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: exit(2) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l6) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 2) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: completeReq(2) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: updateQueue(2) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: updateQueue(2) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: updateQueue(2) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l8) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: checkQueue(2) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: l10) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: resetReq(2) (#req[1]: 3) (#req[2]: 3) (#req[3]: 1) (pc[1]: l5) (pc[2]: rem) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 3)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3))) tran: try(2) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l1) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 2),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(1, priv(empty, (1 : 2),2 : 3))) tran: receiveReq(2) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l1) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(1, priv(empty, (1 : 2),2 : 3))) tran: setReq(2) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l2) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(1, priv(empty, (1 : 2),2 : 3))) tran: checkPriv(2) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l3) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 3) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(1, priv(empty, (1 : 2),2 : 3))) tran: incReqNo(2) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(1, priv(empty, (1 : 2),2 : 3))) tran: sendReq(2) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(1, priv(empty, (1 : 2),2 : 3))) tran: sendReq(2) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ;msg(1, priv(empty, (1 : 2),2 : 3))) tran: sendReq(2) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(1, priv(empty, (1 : 2),2 : 3))) tran: sendReq(2) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 2) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: waitPriv(1) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: cs) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: exit(1) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l6) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 2),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))n    tran: completeReq(1) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: updateQueue(1) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 2) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: updateQueue(1) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 3) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: updateQueue(1) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l8) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: checkQueue(1) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: l10) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: resetReq(1) (#req[1]: 3) (#req[2]: 4) (#req[3]: 1) (pc[1]: rem) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 4)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: try(1) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l1) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 3) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(2, priv(empty, (1 : 3),2 : 3))) tran: receiveReq(1) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l1) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(2, priv(empty, (1 : 3),2 : 3))) tran: setReq(1) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l2) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(2, priv(empty, (1 : 3),2 : 3))) tran: checkPriv(1) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l3) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 3),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(2, priv(empty, (1 : 3),2 : 3))) tran: incReqNo(1) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(2, priv(empty, (1 : 3),2 : 3))) tran: sendReq(1) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 2) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(2, priv(empty, (1 : 3),2 : 3))) tran: sendReq(1) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 3) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(2, priv(empty, (1 : 3),2 : 3))) tran: sendReq(1) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(2, priv(empty, (1 : 3),2 : 3))) tran: sendReq(1) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 2),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: waitPriv(2) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: cs) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: exit(2) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l6) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 3) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: completeReq(2) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: updateQueue(2) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: updateQueue(2) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: updateQueue(2) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l8) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: checkQueue(2) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: l10) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: resetReq(2) (#req[1]: 4) (#req[2]: 4) (#req[3]: 1) (pc[1]: l5) (pc[2]: rem) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 4)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4))) tran: try(2) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l1) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 3),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(1, priv(empty, (1 : 3),2 : 4))) tran: receiveReq(2) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l1) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(1, priv(empty, (1 : 3),2 : 4))) tran: setReq(2) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l2) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(1, priv(empty, (1 : 3),2 : 4))) tran: checkPriv(2) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l3) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 4) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(1, priv(empty, (1 : 3),2 : 4))) tran: incReqNo(2) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(1, priv(empty, (1 : 3),2 : 4))) tran: sendReq(2) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(1, priv(empty, (1 : 3),2 : 4))) tran: sendReq(2) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(1, priv(empty, (1 : 3),2 : 4))) tran: sendReq(2) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(1, priv(empty, (1 : 3),2 : 4))) tran: sendReq(2) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 3) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: waitPriv(1) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: cs) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: exit(1) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l6) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 3),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: completeReq(1) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: updateQueue(1) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 2) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: updateQueue(1) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l7) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 3) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: updateQueue(1) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l8) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: checkQueue(1) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: l10) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: resetReq(1) (#req[1]: 4) (#req[2]: 5) (#req[3]: 1) (pc[1]: rem) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 5)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: try(1) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l1) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: true) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 4) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(2, priv(empty, (1 : 4),2 : 4))) tran: receiveReq(1) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l1) (pc[2]: l5) (pc[3]: l4) (requesting[1]: false) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(2, priv(empty, (1 : 4),2 : 4))) tran: setReq(1) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l2) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(2, priv(empty, (1 : 4),2 : 4))) tran: checkPriv(1) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l3) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 4),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(2, priv(empty, (1 : 4),2 : 4))) tran: incReqNo(1) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(2, priv(empty, (1 : 4),2 : 4))) tran: sendReq(1) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 2) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(2, priv(empty, (1 : 4),2 : 4))) tran: sendReq(1) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l4) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 3) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(2, priv(n    empty, (1 : 4),2 : 4))) tran: sendReq(1) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(2, priv(empty, (1 : 4),2 : 4))) tran: sendReq(1) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 3),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: waitPriv(2) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: cs) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: exit(2) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l6) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 4) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: completeReq(2) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: updateQueue(2) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: updateQueue(2) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l7) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: updateQueue(2) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l8) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: checkQueue(2) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: l10) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: resetReq(2) (#req[1]: 5) (#req[2]: 5) (#req[3]: 1) (pc[1]: l5) (pc[2]: rem) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(1, 5)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5))) tran: try(2) (#req[1]: 5) (#req[2]: 6) (#req[3]: 1) (pc[1]: l5) (pc[2]: l1) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: true) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 4),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(1, priv(empty, (1 : 4),2 : 5))) tran: receiveReq(2) (#req[1]: 5) (#req[2]: 6) (#req[3]: 1) (pc[1]: l5) (pc[2]: l1) (pc[3]: l4) (requesting[1]: true) (requesting[2]: false) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 5),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(1, priv(empty, (1 : 4),2 : 5))) tran: setReq(2) (#req[1]: 5) (#req[2]: 6) (#req[3]: 1) (pc[1]: l5) (pc[2]: l2) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 5),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(1, priv(empty, (1 : 4),2 : 5))) tran: checkPriv(2) (#req[1]: 5) (#req[2]: 6) (#req[3]: 1) (pc[1]: l5) (pc[2]: l3) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 5),2 : 5) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(1, priv(empty, (1 : 4),2 : 5))) tran: incReqNo(2) (#req[1]: 5) (#req[2]: 6) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 5),2 : 6) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3) || 
(nw: (msg(1, req(2, 6)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(1, priv(empty, (1 : 4),2 : 5))) tran: sendReq(2) (#req[1]: 5) (#req[2]: 6) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 5),2 : 6) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 2) idx[3]: 3) || 
(nw: (msg(1, req(2, 6)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(1, priv(empty, (1 : 4),2 : 5))) tran: sendReq(2) (#req[1]: 5) (#req[2]: 6) (#req[3]: 1) (pc[1]: l5) (pc[2]: l4) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 5),2 : 6) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 3) idx[3]: 3) || 
nw: (msg(1, req(2, 6)) ; msg(1, req(3, 1)) ; msg(2, req(3, 1)) ; msg(3, req(1, 1)) ; msg(3, req(1, 2)) ; msg(3, req(1, 3)) ; msg(3, req(1, 4)) ; msg(3, req(1, 5)) ; msg(3, req(2, 1)) ; msg(3, req(2, 2)) ; msg(3, req(2, 3)) ; msg(3, req(2, 4)) ; msg(3, req(2, 5)) ; msg(3, req(2, 6)) ; msg(1, priv(empty, (1 : 4),2 : 5))) tran: sendReq(2) (#req[1]: 5) (#req[2]: 6) (#req[3]: 1) (pc[1]: l5) (pc[2]: l5) (pc[3]: l4) (requesting[1]: true) (requesting[2]: true) (requesting[3]: true) (havePriv[1]: false) (havePriv[2]: false) (havePriv[3]: false) (rn[1]: (1 : 5),2 : 5) (rn[2]: (1 : 5),2 : 6) (rn[3]: 3 : 1) (ln[1]: (1 : 4),2 : 4) (ln[2]: (1 : 4),2 : 5) (ln[3]: ia) (queue[1]: empty) (queue[2]: empty) (queue[3]: empty) (idx[1]: 1) (idx[2]: 1) idx[3]: 3