module Circuit2 {
  type Bit = boolean;

  var c1: record { r1: Bit };
  var x2: Bit;
  var y2: Bit;
  var r2: Bit;

  instance c2: Circuit(y1:(c1.r1), y2:(y2));

  next {
    y2' = (x2 || c2.r2);
    r2' = (x2 || c2.r2);

  }
}
module Circuit1 {
  type Bit = boolean;

  var y1: Bit;
  var r1: Bit;

  instance c1: Circuit2();

  next {
    y1' = c1.r1;
    r1' = !c1.r1;

  }
}
module Circuit {
  type Bit = boolean;

  var x2: Bit;
  var r1: Bit;
  var r2: Bit;

  output y1: Bit;
  output y2: Bit;

  instance c1: Circuit1();
  instance c2: Circuit2();

  next {
    y1' = c1.r1;
    r1' = !c1.r1;
    y2' = (x2 || c2.r2);
    r2' = (x2 || c2.r2);

  }
}
