Re: [tlaplus] Debugging endless model checking

Thank you, thats what I've been doing for a while but I was hoping there was an easier way.

On Tuesday, August 6, 2019 at 1:28:29 AM UTC+2, AmirHossein wrote:

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

Hi. Thank you, this helped me to get forward. It seems however that my model is just very state-intensitve. I deduce this from the fact that in the previous version, my diameter was 55. After the recent changes i expect a reasonable increase to at most 70. However, after the change, the diameter slows down radically as it gets to diameter of about 35, which makes me believe that infinite loops are not my problem (then i would have huge diameters). I have also added an invariant which will fail the model if the diameter reaches a certain number. It hasn't yet. I suspect that there is something that explodes my model width-wise.

I am working on improving my model and I've had great success, however not enough yet. It will be interesting to see if it really just was a massive state explosion that caused my problem!

On Tuesday, August 6, 2019 at 2:04:54 AM UTC+2, Hillel Wayne wrote:

Hi Jam,

As of 1.6.0, you can access the diameter, level, etc during model checking via TLCGet. See https://github.com/tlaplus/tlaplus/blob/9dce6c7404552d70f728332c85aaa3af2aed719a/tlatools/src/tlc2/module/TLC.java#L168-L212. You can use this to constrain the model to help with debugging. I'd recommend using the -dump switch and then running the dump through a dedicated graph viewer.

H

On 8/5/19 1:22 PM, Jam 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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/119e0b62-07c6-404b-89f9-a5f1f698ccb5%40googlegroups.com.