TLC: distinct states decreasing?

[Ognjen Maric]

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?

[Markus Kuppe]

This is unexpected. Please open an issue and provide as much information as possible about your environment and how you start TLC.

Thanks,
Markus