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

*From*: Giuliano <giulia...@xxxxxxxxx>*Date*: Tue, 20 Oct 2015 17:21:39 -0700 (PDT)

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

**Follow-Ups**:**Re: Potentially confusing behavior of a PlusCal algorithm***From:*Leslie Lamport

**Re: [tlaplus] Potentially confusing behavior of a PlusCal algorithm***From:*Stephan Merz

**Re: Potentially confusing behavior of a PlusCal algorithm***From:*Leslie Lamport

- Prev by Date:
**Re: Unclear TLC evaluation behavior** - Next by Date:
**Re: Unclear TLC evaluation behavior** - Previous by thread:
**Re: Unclear TLC evaluation behavior** - Next by thread:
**Re: Potentially confusing behavior of a PlusCal algorithm** - Index(es):