[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Missing error trace on invariant violation
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).