module CompositeCircuit {
  var r1_prime: boolean;
  var r2_prime: boolean;
  var y1_prime: boolean;
  var y2_prime: boolean;
  var r1: boolean;
  var r2: boolean;

  input x2: boolean;

  output y1: boolean;
  output y2: boolean;

  init {
    r1 = false;
    r2 = false;

  }
  next {
    y1_prime' = r1;
    r1_prime' = !r1;
    y2_prime' = (x2 || r2);
    r2_prime' = (x2 || r2);
    y1' = y1_prime;
    r1' = r1_prime;
    y2' = y2_prime;
    r2' = r2_prime;

  }
  invariant spec: ((y1 == r1) ==> ??);

}
