module traffic_light1 {
  type state_t = enum { RED, GREEN };

  var state : state_t;
  output green1 : boolean;
  output red1 : boolean;

  init {
    state = RED;
    green1 = false;
    red1 = true;
  }

  next {
    if (state == RED) {
      green1' = true;
      red1' = false;
    } else {
      green1' = false;
      red1' = true;
    }
  }
}

module traffic_light2 {
  type state_t = enum { RED, GREEN };

  var state : state_t;
  output green2 : boolean;
  output red2 : boolean;

  init {
    state = GREEN;
    green2 = true;
    red2 = false;
  }

  next {
    if (state == RED) {
      green2' = false;
      red2' = true;
    } else {
      green2' = true;
      red2' = false;
    }
  }
}

module main {
  var A : boolean; // Action A
  var B : boolean; // Action B

  instance t1 : traffic_light1(green1, red1);
  instance t2 : traffic_light2(green2, red2);

  init {
    A = false;
    B = false;
  }

  next {
    havoc A;
    havoc B;

    if (A && t1.state == traffic_light1.state_t.RED && t2.state == traffic_light2.state_t.GREEN) {
      t1.state' = traffic_light1.state_t.GREEN;
      t2.state' = traffic_light2.state_t.RED;
    }

    if (B && t1.state == traffic_light1.state_t.GREEN && t2.state == traffic_light2.state_t.RED) {
      t1.state' = traffic_light1.state_t.RED;
      t2.state' = traffic_light2.state_t.GREEN;
    }
  }

  invariant no_deadlock : !(t1.state == traffic_light1.state_t.RED && t2.state == traffic_light2.state_t.GREEN && A && !B);

  control {
    check;
    print_results;
  }
}
