[tlaplus] Invariant violated, no state trace

["'Michal Jaszczyk' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2759c5eb-748a-4849-9bdc-da8f23765e7dn%40googlegroups.com.