// Define the module for the sequential circuit
module main {
  // Declare input, output, and register variables
  input x : boolean;
  var r : boolean;
  var y : boolean;

  // Define the initial states S1 and S2
  init {
    // S1: x = 0, r = 0
    // S2: x = 1, r = 0
    // Initial value of r is 0 in both cases
    r = false;
  }

  // Define the next state transitions
  next(r) {
    // next_r = x OR r
    // Once r is 1, it remains 1
    if (r) {
      true;
    } else {
      x || r;
    }
  }

  // Define the output computation
  next(y) {
    // y = !(x XOR r)
    !(x ^ r);
  }

  // Define the LTL property to check that y is set infinitely often
  ltl infinitely_often_y {
    // This LTL formula checks that y is true infinitely often
    G F y;
  }
}

// Instantiate the module and run the model checker
control {
  // Set up the model checker
  main m;
  m.check;
  m.print_results;
}
