[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?


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.