Re: [tlaplus] In TLC, what are "generated" vs "distinct" states?

Still, only 20,608 distinct states were found though. My understanding is that the Next state relation determines what the edges in the state graph can be, not the states themselves (though if certain states are unreachable due to the logic of the relation, of course those wouldn't be in the state graph). But the states are determined by the possible values of the variables. Even in this relation, I'm allowing all possible values for authorizations and leases, so I'm not understanding why my calculation is off. I'm dwelling on it because getting the right number will ensure that my mental model of the state space is correct.

On Thursday, July 30, 2020 at 5:38:22 PM UTC-4 hwa...@xxxxxxxxx wrote:

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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/34163606-c419-4f9e-97ac-6331ce49b642n%40googlegroups.com.