[tlaplus] Re: Invariant violated, no state trace

[Earnshaw <dongluming77@xxxxxxxxx>]

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

在2024年5月30日星期四 UTC+8 01:12:51<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

-- 
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/973cfc56-ae80-41b2-9c2e-733c199363ben%40googlegroups.com.