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

["'Alex Weisberger' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

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.

-- 
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.