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

*From*: cfh...@xxxxxxxxx*Date*: Tue, 3 Oct 2017 22:25:05 -0700 (PDT)

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: DieHarder3 alternative solutions (new user)***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Broken link for TLAPS for MacOS** - Next by Date:
**Re: DieHarder3 alternative solutions (new user)** - Previous by thread:
**Re: Failed to produce PDF using Toolbox 1.5.3** - Next by thread:
**Re: DieHarder3 alternative solutions (new user)** - Index(es):