Invariant violated, no state trace

[Michal Jaszczyk]

Hello,

Typically, when TLC finds something is wrong with my model, I get a trace explaining how the bad state can be reached from the initial state.

I'm currently working on a large model (depth 57, 5B distinct states found, 3 days of runtime). There is something wrong in the model, and TLC aborts with the following message:

Error: Invariant ValidData is violated.
5859583447 states generated, 5767844425 distinct states found, 842437210 states left on queue.
The depth of the complete state graph search is 57.

But there is no state trace. Why is that?

Thanks,

M

[Earnshaw]

You can try to get the error trace log file by using TLC command line instead of ToolBox GUI as the following example

java -cp tla2tools.jar tlc2.TLC -dump MyTraceDumpDir -workers auto -config MySpec.cfg MySpec.tla