c
module main {
    var x: int;

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

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

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

    process P1 = Inc();
    process P2 = Dec();
    process P3 = Reset();

    invariant bounds: 0 <= x && x <= 200;
}
