Re: [tlaplus] Re: DieHarder3 alternative solutions (new user)

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

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