Re: [tlaplus] Re: Error when adding an Invariant

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

On 04.11.2015 00:46, Giuliano wrote:
> Hello, I am using version 1.5.1 of the TLA Toolbox and I still regularly
> get this kind of error.
> Moreover, when checking multiple invariants, TLC sometimes wrongly
> reports the one that is violated.
> For example TLC will report that Inv1 is violated when Inv2 is violated
> and not Inv1.
> Is there something I can do next time it happens to help locate the problem?

Hi Guiliano,

I expect this to be fixed in the upcoming Toolbox release. You can try
today's nightly build [1].

Can you still send me the spec, the .toolbox directory, and the log file
to investigate though?

Thanks
Markus

[1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/