Re: Discrepancy between TLA+ Hyperbook and TLA+ toolbox

[Leslie Lamport <tlapl...@xxxxxxxxx>]

Dear Arunabha,

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.

Leslie

On Tuesday, July 15, 2014 10:33:25 PM UTC-7, Arunabha Ghosh wrote:

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