[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Potentially confusing behavior of a PlusCal algorithm

Hello, consider the following algorithm:

--algorithm Algo1 {
    variables b1 = FALSE, b2 = FALSE
    define {
        B1 == b1
    fair process (stuck \in {"stuck"}) {
        l1: b1 := TRUE;
            await B1;
    fair process (notstuck \in {"notstuck"}) {
        l2: b2 := TRUE;
            await b2;

The process "stuck" will never reach the label "Done", while the process "notstuck" will reach it.
This kind of behavior may cause confusion in a more complex algorithm and I could not find any warning about it in the PlusCal user's manual.