[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Debugging endless model checking

Hello. My model has reached a point where its is quite big. The problem is, that after my latest addition i strongly suspect that it will never finish model checking- I have ran it on 6 cores, 30gb memory for 8 hours, it has generated 40GB of states, but the queue continued growing. As a contrast to this, the model before the change with the same constants took half an hour. The question of this thread is, what techniques can I use to find what causes the model to loop infinitely? This is what I have done so far:
Techniques/things that would be of huge value, would be:
I love your tool and hope it will continue to develop!

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/119e0b62-07c6-404b-89f9-a5f1f698ccb5%40googlegroups.com.