Re: [tlaplus] Error when adding an Invariant

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

On 25.09.2015 17:12, 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


Hi Sowmy,


this is a TLA+ Toolbox bug we thought is fixed in its most recent
version (1.5.1). The Toolbox races to read a data structure while its
being written. Is this reproducible if you re-run the model checker?


> PS: Is TLA tool source available as open source?


Yes, you can find it at
https://tlaplus.codeplex.com/SourceControl/list/changesets?branch=master


Thanks
Markus