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