[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: "'Alex Weisberger' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Thu, 30 Jul 2020 18:28:57 -0700 (PDT)*References*: <34163606-c419-4f9e-97ac-6331ce49b642n@googlegroups.com> <4dbd29c1-d1a2-060b-cbf0-1ace9ffbf4e3@gmail.com>

Thanks for the reply.

You brought up a great point that the spec allowed every state to transition to each other. That definitely blew up the state space. I modified the Next state relation to be a little less extreme:

ChangeAuth == /\ authorizations' \in AuthorizationsType

/\ UNCHANGED leases

/\ viewableTenants' = TenantPolicy

ChangeTenants == /\ UNCHANGED authorizations

/\ leases' \in LeasesType

/\ viewableTenants' = TenantPolicy

Next == \/ ChangeAuth

\/ ChangeTenants

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.

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/fd860144-3b0a-410f-b66b-dae94bce4cccn%40googlegroups.com.

**References**:**[tlaplus] In TLC, what are "generated" vs "distinct" states?***From:*'Alex Weisberger' via tlaplus

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

- Prev by Date:
**Re: [tlaplus] In TLC, what are "generated" vs "distinct" states?** - Next by Date:
**Re: [tlaplus] error trace on assertion failure?** - Previous by thread:
**Re: [tlaplus] In TLC, what are "generated" vs "distinct" states?** - Next by thread:
**[tlaplus] Is it possible to create two separate channels so that they can run separately according to their respective heartbeat timing** - Index(es):