DieHarder3 alternative solutions (new user)

[cfh...@gmail.com]

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

[Leslie Lamport]

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

[Markus Alexander Kuppe]

On 04.10.2017 09:31, Leslie Lamport wrote:
> 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.

Hi Chuck,

you can run TLC with the "-continue" flag. TLC will then continue to
search for all (even shorter) counterexamples if any.

Its downside is, that it corresponds to a complete graph exploration
whereas TLC's by default stops graph exploration after finding the first
counterexample. Note that the Toolbox does not support the "-continue" flag.


TLC achieves significantly better performance by relaxing breadth-first
exploration. This has the side effect that TLC only provides an
approximation of the shortest counterexample with breadth-first. By the
way, depth-first mode is actually depth-first iterative deepening [1].

M.

[1] https://en.wikipedia.org/wiki/Iterative_deepening_depth-first_search