[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Error when adding an Invariant
- From: Sowmy Srinivasan <sow...@xxxxxxxxx>
- Date: Fri, 25 Sep 2015 08:12:42 -0700 (PDT)
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?