module circuit {
  var x : boolean;
  var y : boolean;
  var r : boolean;

  init {
    r = false;
  }

  next {
    if (r == false) {
      r' = x || r;
    } else {
      r' = r;
    }

    y = !(x ^ r);
  }
}

module main {
  instance c : circuit;

  init {
    c.x = false; // initial state S1: x=0, r=0
  }

  transition {
    c.x = true; // transition to initial state S2: x=1, r=0
  }

  ltl property output_set_infinitely_often {
    []<> c.y;
  }
}
