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