automaton TrafficLight is
  states
    Red, Yellow, Green
  initial state Red
  transitions
    Red -> Green on timer(30)
    Green -> Yellow on timer(25)
    Yellow -> Red on timer(5)
  outputs
    emit red_light in Red
    emit yellow_light in Yellow
    emit green_light in Green
end automaton