DieHarder3 alternative solutions (new user)

[cfh...@xxxxxxxxx]

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