# Re: Understanding "OneBitProtocol"

I see, now. The Init state ensures that x \in [{0, 1} -> BOOLEAN], so the process cannot be entered with a null x[self]. Thanks!

On Thursday, February 20, 2014 11:45:31 AM UTC-8, Leslie Lamport wrote:
That paragraph begins by saying that the code "is allowed only to change x[self] and pc[self]".  The sentence you quote should say "the process should not set x[self] to any value other than a Boolean".  It is assumed that, when the code is executed, x[self] will have a Boolean value.  I hope that makes it clear.

Leslie

On Thursday, February 20, 2014 11:10:52 AM UTC-8, Brian Beckman wrote:
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 it
reads 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 an
arbitrarily (nondeterministically) chosen Boolean value:

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

The algorithm should allow this with statement to be executed any number
of times before the process reaches e1. We can express this by letting the while
loop 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..."