module TrafficLightModule {
  type State = enum { GREEN, RED };

  var action: enum { A, B };
  var traffic_light1: State;
  var traffic_light2: State;

  init {
    traffic_light1 = RED;
    traffic_light2 = GREEN;

  }
  next {
    if (action == A) {
      if ((traffic_light1 == RED) && (traffic_light2 == GREEN)) {
        traffic_light1' = GREEN;
        traffic_light2' = RED;
      }
    } else {
      if (action == B) {
        if ((traffic_light1 == GREEN) && (traffic_light2 == RED)) {
          traffic_light1' = RED;
          traffic_light2' = GREEN;
        }
      }
    }

  }
}
