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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Wed, 4 Oct 2017 00:31:37 -0700 (PDT)*References*: <b9564123-4cf1-4afb-8b87-cb99e03d829b@googlegroups.com>

When using multiple worker threads, TLC's state exploration is only approximately breadth-first. I don't know where the DieHarder3 example is, so I can't look at it myself. Please run your model with a single worker thread. (Go to the *How to Run* section of the *Model Overview* page for the setting.) If you still get the same result, please send me the spec (or tell me where it is) and what your model is.

Leslie

On Tuesday, October 3, 2017 at 11:50:46 PM UTC-7, cfharr wrote:

As a brand new TLA user working from the video tutorial, I ran the DieHarder3 example verbatim and got the expected result with a length of 9 steps.

However I had in my head an alternative, shorter solution (7 steps). I could get the Model Checker to generate this solution by selecting "Depth-first" in the TLC options.

This appears to conflict with the Help Text statement under "TLC Options - Model Checking Mode" :

[...]Its default method of doing this is to find the graph of all reachable states using breadth-first search. This has the advantage that if TLC finds a violation of a safety property, then it will produce a shortest possible behavior that exhibits the error.

Perhaps that statement about "breadth-first" algorithm results is wrong?

Chuck

**Follow-Ups**:**Re: [tlaplus] Re: DieHarder3 alternative solutions (new user)***From:*Markus Alexander Kuppe

**References**:**DieHarder3 alternative solutions (new user)***From:*cfh . . .

- Prev by Date:
**DieHarder3 alternative solutions (new user)** - Next by Date:
**NFM 2018: 2nd Call for Papers (extended deadlines)** - Previous by thread:
**DieHarder3 alternative solutions (new user)** - Next by thread:
**Re: [tlaplus] Re: DieHarder3 alternative solutions (new user)** - Index(es):