
module weather_station {
  // Define variables
  var temp : int;
  var count : int;
  const threshold : int = 25; // Example threshold

  // Initialize variables
  init {
    temp = 20; // Initial temperature
    count = 0; // Initial count
  }

  // Define the transition relation
  next {
    // Simulate reading a new temperature
    temp' = temp + 1 - 2 * (temp % 5); // Example transition, fluctuating temperature

    // Increment count if the new temperature exceeds the threshold
    if (temp' > threshold) {
      count' = count + 1;
    } else {
      count' = count;
    }
  }

  // Optional: Define an invariant to ensure count is non-decreasing
  invariant count_is_non_decreasing : count' >= count;

  // Control block for simulation or bounded model checking
  control {
    v = simulate 10; // Simulate 10 steps
    print_trace;
  }
}
