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

*From*: "'Alex Weisberger' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Wed, 29 Jul 2020 19:57:37 -0700 (PDT)

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.

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

- Prev by Date:
**Re: [tlaplus] PlusCal Translation problem** - Next by Date:
**Re: [tlaplus] In TLC, what are "generated" vs "distinct" states?** - Previous by thread:
**Re: [tlaplus] PlusCal Translation problem** - Next by thread:
**Re: [tlaplus] In TLC, what are "generated" vs "distinct" states?** - Index(es):