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?
Giuliano
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?
Thanks
Sowmy
PS: Is TLA tool source available as open source?