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):
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, ...).
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/
For more options, visit https://groups.google.com/d/