module TrafficLight {
  type state_type = enum { green, red };

  var current_state: state_type;

  init {
    current_state = red;

  }
  next {
    if (current_state == red) {
      current_state' = green;
    } else {
      current_state' = red;
    }

  }
  invariant spec: ((current_state == red) || (current_state == green));

}
