module TrafficLightModule {
  var red1: boolean;
  var green1: boolean;
  var red2: boolean;
  var green2: boolean;

  init {
    red1 = true;
    green1 = false;
    red2 = true;
    green2 = false;

  }
  next {
    if (red1) {
      green1' = true;
      red1' = false;
    } else {
      green1' = false;
      red1' = true;
    }
    if (red2) {
      green2' = true;
      red2' = false;
    } else {
      green2' = false;
      red2' = true;
    }

  }
  control {
    induction(1);
    check;
    print_results;

  }
}
