[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
DieHarder3 alternative solutions (new user)
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?