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

*From*: Giuliano <giulia...@xxxxxxxxx>*Date*: Tue, 3 Nov 2015 15:46:09 -0800 (PST)*References*: <a3a0946e-c452-4744-8495-eefd46589b04@googlegroups.com>

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:

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?

**Follow-Ups**:**Re: [tlaplus] Re: Error when adding an Invariant***From:*Markus Alexander Kuppe

**References**:**Error when adding an Invariant***From:*Sowmy Srinivasan

- Prev by Date:
**Re: Examples using Reals?** - Next by Date:
**Re: Examples using Reals?** - Previous by thread:
**Re: [tlaplus] Error when adding an Invariant** - Next by thread:
**Re: [tlaplus] Re: Error when adding an Invariant** - Index(es):