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:
- I have set state constraints on variables which could grow infinitely. This has not fixed the problem
- I have tried using the TLC switch -dump for dumping the states into a file, just to make sure that everything is in order (nothing being cluttered with values or abnormally big)
- I have tried lowering the constants. The model did finish checking for constants that are too small to provide any valuable information (minimal value for my constant should be 1..3, it only passed for 1..2). This makes me a bit pessimistic, thinking that I am faced against extreme state explosion.
Techniques/things that would be of huge value, would be:
- Some way of printing stack traces for where there are X or more actions taken.
- What are the criteria for liveness checking giving false results when using symmetry sets? My model would greatly benefit from them, but liveness checking is essential for me
- Maybe some other ideas?
- How do you start a depth-first with depth limit using the TLC for consoles? The -depth switch seems to be a switch for simulation (src: https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/tlc2/TLC.java)
I love your tool and hope it will continue to develop!