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.
Hi Lorin,
the underlying TLC bug is fixed with commit
4edafdb693a65c5aefcda8be527f303eafdae32a [1]. You can grab a nightly
Toolbox build [2] 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
[1]
https://github.com/tlaplus/tlaplus/commit/4edafdb693a65c5aefcda8be527f303eafdae32a
[2] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/
Thanks, Markus. The latest nightly build has resolved the issue for me.
Take care,
Lorin