!(police.state=go_A_init);
!(police.state=go_B_init);
!(road_A.state=STOPPED_init);
!(road_B.state=STOPPED_init);