module C1 {
  output y1 : boolean;
  register r1 : boolean;

  next {
    y1' = r1;
    r1' = !r1;
  }
}

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

  next {
    y2' = x2' | r2;
    r2' = x2' | r2;
  }
}

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

  init {
    assume(true);
  }

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