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