---- MODULE TrafficCrossingTest ----
EXTENDS TrafficCrossing
TestYellow == \E road \in Roads : lights[road] = "yellow"
TestRedYellow == \E road \in Roads : lights[road] = "redyellow"
TestCarCrosses == \E c \in Cars : cars[c].pos = 0
=============================================================================