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

Re: Potentially confusing behavior of a PlusCal algorithm



Please explain what you find confusing about this.


Thanks,

Leslie


On Tuesday, October 20, 2015 at 5:21:39 PM UTC-7, Giuliano wrote:
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.

Cheers,
Giuliano