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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 17 Jul 2014 01:27:30 -0700 (PDT)*References*: <1b27d56e-eda5-45f8-b31e-5f24295b4cb3@googlegroups.com>

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 bTypeOk == (b = 0) \/ (b = 1)Init1 == (b = 0) \/ (b = 1)Next1 == \/ /\ b = 0/\ b' = 1\/ /\ b = 1/\ b' = 0However 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 = 1Funnily 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

**References**:**Discrepancy between TLA+ Hyperbook and TLA+ toolbox***From:*Arunabha Ghosh

- Prev by Date:
**Discrepancy between TLA+ Hyperbook and TLA+ toolbox** - Next by Date:
**Execution semantics of \/** - Previous by thread:
**Discrepancy between TLA+ Hyperbook and TLA+ toolbox** - Next by thread:
**Execution semantics of \/** - Index(es):