Re: [tlaplus] About single process system, fairness, and depth-first search option

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

On 20.12.2016 08:54, Stephan Merz wrote:
> As for your question about depth-first vs. breath-first search, in my
> experiments depth-first search never finished on your example in the
> sense that the progress bar was still being displayed without any
> notable processor activity. Maybe a TLC expert can explain what's
> happening. I cannot tell what the "result" of these runs was.


Hi,

this is a bug in TLC's depth-first search. TLC's never terminates which
is why the Toolbox does not show the final model checking result. The
bug goes back to at least TLC version 2.03 released 2011.

Until we have a fix, you can instruct TLC to use a single worker as a
workaround.

Cheers

Markus