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

*From*: Brian Beckman <bc.be...@xxxxxxxxx>*Date*: Thu, 20 Feb 2014 11:10:52 -0800 (PST)

I'm working on understanding the one-bit protocol in the "Principles" section of the hyperbook, and have a question about the following construction. The book says on page 10:

Since we don't want to worry about what the other process might do if itreads x[self] to be a non-Boolean value, the process should set x[self]to a Boolean. Here is a PlusCal statement that sets x[self] to anarbitrarily (nondeterministically) chosen Boolean value:

with (v \in BOOLEAN ) { x[self] = v }...

The algorithm should allow this with statement to be executed any numberof times before the process reaches e1. We can express this by letting the whileloop begin:

r : while(true){ either { with (v \in BOOLEAN ) { x[self] = v } ;goto r}or skip ;

...

Doesn't this code allow the statement to be executed zero times, in particular, if the "or skip" is nondeterministically chosen? If so, can't we reach later code with x[self] having no value, in particular, no Boolean value? If so, doesn't that defeat the purpose of the construction, which is "... set x[self] to a Boolean..."

**Follow-Ups**:**Re: Understanding "OneBitProtocol"***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Re: position of PlusCal assert in Euclid from Hyperbook?** - Next by Date:
**Re: Understanding "OneBitProtocol"** - Previous by thread:
**A typo in hyperbook** - Next by thread:
**Re: Understanding "OneBitProtocol"** - Index(es):