|
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 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.
--
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/2db5061b-2735-7a30-fb50-832caf890322%40gmail.com.
|