module TrafficLights {
  var green1: boolean;
  var green2: boolean;
  var next_green1: boolean;
  var next_green2: boolean;
  var next_red1: boolean;
  var next_red2: boolean;
  var red1: boolean;
  var red2: boolean;
  var traffic_light1: boolean;
  var traffic_light2: boolean;

  init {
    traffic_light1 = red1;
    traffic_light2 = green2;

  }
  next {
    if (traffic_light1 && traffic_light2) {
      next_green1' = (traffic_light1 && green1);
      next_red1' = !next_green1;
      next_green2' = !green2;
      next_red2' = !next_green2;
    } else {
      if (!traffic_light1 && !traffic_light2) {
        next_green1' = !green1;
        next_red1' = !next_green1;
        next_green2' = (traffic_light2 && green2);
        next_red2' = !next_green2;
      } else {
        if (traffic_light1 && !traffic_light2) {
          next_green1' = (traffic_light1 && green1);
          next_red1' = !next_green1;
          next_green2' = !green2;
          next_red2' = !next_green2;
        } else {
          if (!traffic_light1 && traffic_light2) {
            next_green1' = !green1;
            next_red1' = !next_green1;
            next_green2' = (traffic_light2 && green2);
            next_red2' = !next_green2;
          }
        }
      }
    }
    green1' = next_green1;
    red1' = next_red1;
    green2' = next_green2;
    red2' = next_red2;

  }
}
