[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Re: Error when adding an Invariant
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?
I expect this to be fixed in the upcoming Toolbox release. You can try
today's nightly build .
Can you still send me the spec, the .toolbox directory, and the log file
to investigate though?