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