[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Discrepancy between TLA+ Hyperbook and TLA+ toolbox
I suspect that the diameter TLC computes is defined to be the smallest N such that every reachable state is reached from an initial state by a path containing at most N nodes. I would appreciate it if you could check this by experimentation. Be aware that TLC is guaranteed to compute the true diameter only if run with a single worker thread.
On Tuesday, July 15, 2014 10:33:25 PM UTC-7, Arunabha Ghosh wrote:
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.
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 ?