In TLC, what are "generated" vs "distinct" states?

[Alex Weisberger]

Consider the following spec:

--------------------- MODULE TenantPermissionsOptimized ---------------------

CONSTANTS Tenants, UserSubject, OtherUser, Assets, ReadOnly, 

          AvailOnly, AvailExist, Available, NotAvailable

VARIABLES authorizations, leases, viewableTenants

Users == { UserSubject, OtherUser }

AccessLevels == { ReadOnly, AvailOnly, AvailExist }

AuthorizationsType == SUBSET [

    user: Users,

    assets: Assets,

    accessLevel: AccessLevels

]

LeasesType == SUBSET [

    tenant: Tenants,

    asset: Assets

]

TenantPolicy == {}

Next == /\ authorizations' \in AuthorizationsType

              /\ leases' \in LeasesType

              /\ viewableTenants' = TenantPolicy

        

Init == /\ authorizations = {}

            /\ leases = {}

            /\ viewableTenants = {}

=============================================================================

For background, I'm trying to simulate a data authorization system. In my mind, the number of states in this model would be the cardinality of the product of the 3 variables' sets, i.e.: 

|authorizations| * |leases| * |viewableTenants|

= 2^3UA * 2^TA * 1

Where U, A, and T are the number of Users, Assets, and Tenants specified in the model. With U=2, A=2, and T=2, this should be:

2^12 * 2^4 = 65,536 states.

Here's an example line from the log when running TLC:

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? And why is the number of generated states so much larger?

Thanks.

[Hillel Wayne]

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

[Alex Weisberger]

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.