//This file was generated from UPPAAL 3.5.7, Jun 2005

/*

*/
(f & (1 << RECSTART)) -->\
(    ((node0.D or node0.D0 or node0.T) imply (not (node1.D or node1.D0 or node1.T or node2.D or node2.D0 or node2.T or node3.D or node3.D0 or node3.T)))\
 and ((node1.D or node1.D0 or node1.T) imply (not (node0.D or node0.D0 or node0.T or node2.D or node2.D0 or node2.T or node3.D or node3.D0 or node3.T)))\
 and ((node2.D or node2.D0 or node2.T) imply (not (node0.D or node0.D0 or node0.T or node1.D or node1.D0 or node1.T or node3.D or node3.D0 or node3.T)))\
 and ((node3.D or node3.D0 or node3.T) imply (not (node0.D or node0.D0 or node0.T or node1.D or node1.D0 or node1.T or node2.D or node2.D0 or node2.T)))\
 and not (f & (1 << RECSTART)) and (f & (1 << RECPROC)) and rec_time == 0)