[tlaplus] Question about OneBitClock example in TLA Hyperbook

[ns <nedsri1988@xxxxxxxxx>]

Here is the one bit clock example:

VARIABLE b

Init1 == (b=0) \/ (b=1)

 

Next1 == \/ /\ b = 0

            /\ b' = 1

         \/ /\ b = 1

            /\ b' = 0

So the text asks us to change the last line from b' = 0 to b' = "xyz". The model checker complains and the explanation given is that it cannot prove that "xyz" = 0. But how does it conclude that there isn't another state "xyz"? Interestingly the following paragraph then verifies that the only states are 0 and 1. 

thanks

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.