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

    // Initialize x with an arbitrary value within the range [0, 200]
    init {
        x = choose i : int :: i >= 0 && i <= 200;
    }

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

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

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

    // Main execution block
    init {
        // Start the concurrent processes
        async call Inc();
        async call Dec();
        async call Reset();
    }

    // Invariant to check the range of x
    invariant x_range : x >= 0 && x <= 200;
}
