module traffic_light(event tick) returns (red, yellow, green)
initial
  red = true;
  yellow = false;
  green = false;
state
  next(red) = yellow;
  next(yellow) = green;
  next(green) = red;
end module