module main {
    type state_t = enum { IDLE, WAIT, CRITICAL };
    var b1 : boolean;
    var b2 : boolean;
    var x : [1..2];
}

init {
    b1 = false;
    b2 = false;
    x = 1;
}

procedure P1() {
    if (b1 == false) {
        b1 := true;
        x := 2;
    }
    else if (x == 1 || !b2) {
        b1 := false;
    }
}

procedure P2() {
    if (b2 == false) {
        b2 := true;
        x := 1;
    }
    else if (x == 2 || !b1) {
        b2 := false;
    }
}

next {
    choose {
        call P1();
        call P2();
    }
}

// Safety property
invariant "mutual_exclusion" (b1 && b2) == false;

// Bounded model checking
control {
    check;
    print_cex;
}
}
