module main {
  // Define the state variables
  var temp : int;
  var count : int;

  // Define the temperature threshold constant
  const THRESHOLD : int = 25;

  // Initialize the state variables
  init {
    temp = nondet(); // Initialize temp with a non-deterministic value
    count = 0;       // Initialize count to zero
  }

  // Transition function to update the state variables
  next {
    temp' = nondet(); // Update temp with a new non-deterministic value
    if (temp' > THRESHOLD && temp <= THRESHOLD) {
      count' = count + 1; // Increment the count if temp rises above the threshold
    } else {
      count' = count; // Keep the count unchanged
    }
  }

  // Control block for bounded model checking
  control {
    v = unroll(10); // Unroll the transition 10 times
    check;          // Check for any assertions or invariants
    print_results;  // Print the results of the checks
  }
}
