Write the state for a traffic light. Fill in the two TODO definitions in
starter.tla, then click Run Model Checker.
TypeOK: color is always one of "red", "green", or "yellow".Init: the light always starts "red".Next is given to you as UNCHANGED color — a light that never changes is
a perfectly valid (if boring) system. You'll make it actually cycle through
its colors in the next chapter.