[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Error when adding an Invariant

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?


On Friday, September 25, 2015 at 11:12:43 AM UTC-4, Sowmy Srinivasan wrote:
I am new to TLA Plus. I am writing a model for some replication stuff I am working on. When I add an Invariant property to the model checker I get the following error.
Invariant 'No value in valueList [] for 0. Bug in TLCModelLaunchDataProvider.' is violated by the initial state:

Console has the following:
@!@!@STARTMSG 2107:1 @!@!@
Invariant inv_14431923173141960000 is violated by the initial state:

Can someone throw light on what this error means?
PS: Is TLA tool source available as open source?