###keys
queue pc[p1] pc[p2] tmp[p1] tmp[p2]

###textDisplay
queue::::REV::::_ _
tmp[p1]::::REV::::_ _
tmp[p2]::::REV::::_ _

###states
(queue: empty (pc[p1]: rs) (pc[p2]: rs) (tmp[p1]: empty) tmp[p2]: empty) || 
(queue: (p1 empty) (pc[p1]: ws) (pc[p2]: rs) (tmp[p1]: empty) tmp[p2]: empty) || 
(queue: (p1 p2 empty) (pc[p1]: ws) (pc[p2]: ws) (tmp[p1]: empty) tmp[p2]: empty) || (queue: (p1 p2 empty) (pc[p1]: cs) (pc[p2]: ws) (tmp[p1]: empty) tmp[p2]: empty) || (queue: (p1 p2 empty) (pc[p1]: ds) (pc[p2]: ws) (tmp[p1]: p2 empty) tmp[p2]: empty) || (queue: (p2 empty) (pc[p1]: rs) (pc[p2]: ws) (tmp[p1]: p2 empty) tmp[p2]: empty) || (queue: (p2 empty) (pc[p1]: rs) (pc[p2]: cs) (tmp[p1]: p2 empty) tmp[p2]: empty) || (queue: (p2 empty) (pc[p1]: rs) (pc[p2]: ds) (tmp[p1]: p2 empty) tmp[p2]: empty) || (queue: (p2 p1 empty) (pc[p1]: ws) (pc[p2]: ds) (tmp[p1]: p2 empty) tmp[p2]: empty)

###loop
(queue: empty (pc[p1]: ws) (pc[p2]: rs) (tmp[p1]: p2 empty) tmp[p2]: empty) || 
(queue: (p2 empty) (pc[p1]: ws) (pc[p2]: ws) (tmp[p1]: p2 empty) tmp[p2]: empty) || (queue: (p2 empty) (pc[p1]: ws) (pc[p2]: cs) (tmp[p1]: p2 empty) tmp[p2]: empty) || (queue: (p2 empty) (pc[p1]: ws) (pc[p2]: ds) (tmp[p1]: p2 empty) tmp[p2]: empty)