[tlaplus] TLC: distinct states decreasing?

[Ognjen Maric <ognjen.maric@xxxxxxxxx>]

Hi,

I have a large model that I'm analyzing using TLC and I occasionally see output such as:

Progress(57) at 2023-11-10 13:37:27: 108,878,998,909 states generated (217,210 s/min), 14,705,581,149 distinct states found (26,032 ds/min), 959,637,472 states left on queue.
Progress(57) at 2023-11-10 13:38:27: 108,878,998,909 states generated (0 s/min), 14,705,581,149 distinct states found (0 ds/min), 959,637,472 states left on queue.
Progress(57) at 2023-11-10 13:39:27: 108,878,998,909 states generated (0 s/min), 14,709,360,255 distinct states found (3,779,106 ds/min), 959,637,472 states left on queue.
Progress(57) at 2023-11-10 13:40:27: 108,892,458,107 states generated (13,459,198 s/min), 14,707,396,636 distinct states found (-1,963,619 ds/min), 959,587,271 states left on queue.

Note that the number of distinct states goes down in the last line of output, and the "distinct states per minute" number is negative. Such output always seems to be preceded by a few lines (i.e., few minutes) of not finding any new states. This could be JVM garbage collection kicking in (as the process is hitting the JVM heap limit size), or perhaps some internal magic since the model uses both SYMMETRY reductions and a VIEW.

Is this behavior something known/expected, or should I be worried about the soundness of the analysis result?

-- 
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/9bfe63c3-da57-4e8c-831e-63eb9592c6c0n%40googlegroups.com.