[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Missing error trace on invariant violation
On Thursday, September 28, 2017 at 4:12:01 PM UTC-5, Markus Alexander Kuppe wrote:
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.
the underlying TLC bug is fixed with commit
4edafdb693a65c5aefcda8be527f303eafdae32a . You can grab a nightly
Toolbox build  or - as a workaround - increase maxSetSize to a value
that is larger than the cardinality of the set of
initial states ("cardinality of the largest enumerable set" on the
advanced options page of the model editor).
Thanks, Markus. The latest nightly build has resolved the issue for me.