module main {
    var x : integer;

    init {
        x = choose i : integer :: i >= 0 && i <= 200;
    }

    // Define the process Inc
    procedure Inc() {
        while (true) {
            if (x < 200) {
                x := x + 1;
            }
        }
    }

    // Define the process Dec
    procedure Dec() {
        while (true) {
            if (x > 0) {
                x := x - 1;
            }
        }
    }

    // Define the process Reset
    procedure Reset() {
        while (true) {
            if (x == 200) {
                x := 0;
            }
        }
    }

    // Non-deterministic scheduler
    procedure Scheduler() {
        while (true) {
            choose {
                call Inc();
                call Dec();
                call Reset();
            }
        }
    }

    // Invariant
    invariant x >= 0 && x <= 200;

    // Main control block
    control {
        check;
        print_cex;
    }
}
