Re: [tlaplus] Missing error trace on invariant violation

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

On 27.09.2017 04:31, Lorin Hochstein wrote:
> Sometimes when I run the TLC Model Checker, it reports "Invariant Inv
> is violated", but there is no error-trace. Under what conditions does
> the checker not show an error trace?
>
> In some cases, when I reduce the size of the model, if the invariant
> is violated than a trace is available. However, in other cases I can't
> reproduce the error with a smaller model.
>
> Here's an example where this happens for me (The TLC model options I'm
> using appear at the bottom of the email):


Hi Lorin,

are you saying that with your ConcurrentUpdates spec and the given
model, the Toolbox never shows an error trace? Or does it fail to show
the trace intermittently hinting at a concurrency bug?

I tried you example ConcurrentUpdates locally with version 1.5.3 of the
Toolbox on Mac, Win and Linux and it showed an error trace every time.

Please provide more information about your environment (OS, Java
version, Toolbox version, ...).

Thanks

Markus