Re: [tlaplus] Debugging endless model checking

Hi,

You can set the profiling option equal to "on" in TLC's advanced options so that you can observe how many times each action in your spec is being taken.

You may try making small edits in your spec and see how the model checking makes progress with each change. This is a lovely little cat and mouse game that you will have to solve.

As another means of "debugging" your spec, you may define and set an invariant in your spec and let TLC check it. You then can violate this invariant deliberately at certain points in your spec that you suspect may be the source of error. This will cause TLC to print a useful sequence of states that may help you catch the error.

During the process of model checking, if the queue of states keeps growing at a steady rate for a considerably long amount time, then there is a high probability that your spec has an error.

Regards,

AmirHossein

On Mon, Aug 5, 2019, 10:52 PM Jam <wawrzynchonewicz@xxxxxxxxx> wrote:

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!

--
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.