
module traffic_light1
{
  var red1 : boolean;
  var green1 : boolean;

  init {
    red1 = true;
    green1 = false;
  }

  transition {
    red1' = green1;
    green1' = red1;
  }
}

module traffic_light2
{
  var red2 : boolean;
  var green2 : boolean;

  init {
    red2 = false;
    green2 = true;
  }

  transition {
    red2' = green2;
    green2' = red2;
  }
}

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

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

  init {
    A = false;
    B = false;
  }

  transition {
    call t1; call t2;
  }

  invariant no_deadlock : !(t1.red1 && t2.red2) && !(t1.green1 && t2.green2);
}
