module traffic_light
{
  type light_t = enum { RED, GREEN };

  var traffic_light1, traffic_light2 : light_t;
  var green1, red1, green2, red2 : boolean;

  init {
    traffic_light1 = RED;
    traffic_light2 = GREEN;
    green1 = false;
    red1 = true;
    green2 = true;
    red2 = false;
  }

  transition {
    // Traffic light 1 transitions
    if
      :: traffic_light1 == RED && traffic_light2 == GREEN -> {
        traffic_light1' = GREEN;
        traffic_light2' = RED;
        green1' = true;
        red1' = false;
        green2' = false;
        red2' = true;
      }
      :: traffic_light1 == GREEN && traffic_light2 == RED -> {
        traffic_light1' = RED;
        traffic_light2' = GREEN;
        green1' = false;
        red1' = true;
        green2' = true;
        red2' = false;
      }
    fi
  }
}

module main
{
  var deadlock : boolean;

  instance t1 : traffic_light;
  instance t2 : traffic_light;

  init {
    deadlock = false;
  }

  next {
    next(t1);
    next(t2);

    // Check for deadlock
    deadlock = (t1.traffic_light1 == t1.traffic_light2) &&
               (t1.traffic_light1 == t2.traffic_light1) &&
               (t1.traffic_light1 == t2.traffic_light2);
  }

  control {
    v = unroll(10);
    check deadlock;
    print_results;
  }
}
