Hi Alex,
Progress(3) at 2020-07-29 22:49:26: 205,670,494 states generated (87,098,882 s/min), 20,608 distinct states found (0 ds/min), 17,465 states left on queue.
So ~205 million states are being "generated", and 20,608 distinct states are found. Why is this such a smaller number than the 65,536 that I think I should be getting?
It's not finished running yet; there are still at least 17,465
states left to check. Presumably, if it finished, it'd give you
the expected number of distinct states.
And why is the number of generated states so much larger?
Currently the spec permits any state to follow any other state. So there are ≈ 2^16*(2^16) 2-step behaviors, ≈ 2^16*(2^16)*2^16 3-step behaviors, etc. TLC is doing an exhaustive search, and while each behavior it explores will be unique, it will visit states it has already seen before (possibly states it saw in other behaviors). That's why you're generating almost 90mm new states per minute, of which 0 are distinct.
H
--
Thanks.--
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/34163606-c419-4f9e-97ac-6331ce49b642n%40googlegroups.com.