Traffic Light Cycle

Write the real Next for the traffic light: fill in the TODO in starter.tla so the light cycles "red" → "green" → "yellow" → "red", forever, then click Run Model Checker.

Use the bulleted \/ style from this lesson — one line per possible transition:

Next ==
  \/ color = "red" /\ color' = ...
  \/ ...

TLC should find exactly 3 reachable states and report no errors. If you see a deadlock, some color has nowhere to go — check every color is covered by one of your bullets.