module main {
    // Shared variable
    var x : integer;

    // Initialization
    init {
        // x can start with any value within the range [0, 200]
        assume(x >= 0 && x <= 200);
    }

    // Process Inc
    procedure Inc() {
        if (x < 200) {
            x := x + 1;
        }
    }

    // Process Dec
    procedure Dec() {
        if (x > 0) {
            x := x - 1;
        }
    }

    // Process Reset
    procedure Reset() {
        if (x == 200) {
            x := 0;
        }
    }

    // Main execution loop simulating potential interleaving
    next {
        choice {
            call Inc();
        } or {
            call Dec();
        } or {
            call Reset();
        }
    }

    // Invariant to ensure x remains within the specified range
    invariant x_range : x >= 0 && x <= 200;

    // Control block for simulation or bounded model checking
    control {
        v = simulate 100;
        print_trace;
        check;
        print_results;
    }
}
