#.include crd.fairness
!(police.state=go_A_init);
!(police.state=go_B_init);
!(road_A.state=STOPPED_init);
!(road_B.state=STOPPED_init);


#.properties
#.automaton /usr/lib/blah/blah
#.blifmv safety.mv
#.connections(status_A=status_A, status_B=status_B)
#.state st1 = state:GOOD
#.posfair
#.subsets {st1}
#.endfair
#.endautomaton
#.endproperties
!(col.state=GOOD);