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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Tue, 20 Oct 2015 23:41:25 -0700 (PDT)*References*: <4d003c31-6b8c-4782-8885-65649ffe5fbe@googlegroups.com>

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 = FALSEdefine {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

**References**:**Potentially confusing behavior of a PlusCal algorithm***From:*Giuliano

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