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

Discrepancy between TLA+ Hyperbook and TLA+ toolbox



Hi,
     I just got started with TLA+ and am reading the hyperbook. I entered the OneBitClock example in TLA+ toolbox exactly as specified in the hyperbook.

VARIABLE b
TypeOk == (b = 0) \/ (b = 1) 

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

However running the ModelChecker produces a report that says that the diameter is 1 rather than 2 as the hyperbook suggests. Thinking about it, the diameter should indeed be 2 in both b = 0 -> b = 1 -> b = 0 and b = 1 -> b = 0 -> b = 1

Funnily enough, changing the initial formula to (b = 0) \/ ((b = 1) /\ (2 = b)) results in a diameter of 2. 

Has anyone else had this problem ?  


Arunabha