// Sequential Circuit Model
module main {
  // Declare the input, output, and register variables
  input x : boolean;
  var y : boolean;
  var r : boolean;

  // Initial state specification
  init {
    r = false;
  }

  // State transition function
  next(r) {
    r' = x | r;
  }

  // Output function
  next(y) {
    y' = !(x ^ r);
  }

  // Initial states (S1 and S2)
  init {
    (x == false && r == false) | (x == true && r == false);
  }

  // LTL property to check if 'y' is set infinitely often
  ltl y_infinitely_often {
    G F y
  }

  // Control block for model checking
  control {
    check;
    print_results;
  }
}
