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

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



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.