
module C1
{
  var y1 : boolean; // output variable
  var r1 : boolean; // register variable

  init {
    r1 = false; // initial value of register r1
    y1 = false; // initial value of output y1
  }

  next {
    y1' = r1; // control function for output y1
    r1' = !r1; // control function for register r1
  }
}

module C2
{
  var x2 : boolean; // input variable
  var y2 : boolean; // output variable
  var r2 : boolean; // register variable

  init {
    r2 = false; // initial value of register r2
    y2 = false; // initial value of output y2
  }

  next {
    y2' = x2 | r2; // control function for output y2
    r2' = x2 | r2; // control function for register r2
  }
}

module synchronous_composition
{
  instance c1 : C1(y1, r1);
  instance c2 : C2(x2, y2, r2);

  init {
    // No specific initialization required for synchronous composition
  }

  next {
    next(c1);
    next(c2);
  }
}
