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

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

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

    // Transition function to update temperature and count
    next {
        // Simulate a temperature change (could be more complex in a real scenario)
        temp' = temp + choose(-2, -1, 0, 1, 2);

        // Increment count if the temperature rises above the threshold
        if (temp' > threshold && temp <= threshold) {
            count' = count + 1;
        } else {
            count' = count;
        }
    }

    // Safety property to ensure count behaves as expected
    invariant count_non_decreasing : count' >= count;
    invariant count_increments_correctly : (temp' > threshold && temp <= threshold) => (count' == count + 1);

    // Control block to simulate and check the model
    control {
        v = simulate(10);  // Simulate 10 steps
        print_trace;
    }
}
