Attempted to construct a set with too many elements (>1000000).

Hello,

I have a problem, when I try check an assumption on record type with a large number of fields:

The relevant part of my model is in definition t_salesf_Lead

t_salesf_Lead == [
Id: d_lead_id,
IsDeleted: d_not_used,
MasterRecordId: d_not_used,
LastName: d_not_used,
FirstName: d_not_used,
\* ....
NumberofLocations__c: d_not_used,
pet_tag__c: d_not_used
] \* definition 'salesf_Lead'

with sets

d_lead_id = { "d_lead_id_1", "d_lead_id_2" } \cup {Nil}
d_not_used    == { "d_not_used_1" } \cup {Nil}

The error is raise in the assumption 'Assume_Lead_Domains'

Assume_Lead_Domains ==
                      Assume_CorrectDomain( t_Lead, "id", d_lead_id )
ASSUME Assume_Lead_Domains

which uses operator 'Assume_CorrectDomain'

Assume_CorrectDomain( set, field, domain ) == { p[field] : p \in set } = domain

I have tried following 'tricks' with no success

\* Attempted to construct a set with too many elements (>1000000)
Assume_CorrectDomain( set, field, domain ) == (CHOOSE x \in set : TRUE)[field] \in domain

\* A non-function (a set of the form [d1 : S1, ... , dN : SN]) was applied as a function.
Assume_CorrectDomain( set, field, domain ) == set[field] = domain

\* Overflow when computing the number of elements in:
Assume_CorrectDomain( set, field, domain ) == IF Cardinality( set ) > 100
                                                THEN Print( << "Set cardinality exceeded ", Cardinality( set ), " continue" >>, TRUE )
                               ELSE { p[field] : p \in set } = domain

The complete model can be found in gist https://gist.github.com/jarjuk/ff81790411095fca5b08fb7a9111b2d7

Questions: Is possible somehow to extract the set defining the type of a record field from the record type definition?
1) In current TLA+ implementation 2) in some future TLA+ implementation 3) theoretically?

Some background information what I am trying to achieve:

I am currently implementing a generator to create TLA+ models for modeling business IT
as explained in a blog entry https://jarjuk.wordpress.com/2016/03/03/sbuilder-2-intro/

One of tasks in the model generation is mapping interface operation parameters to domains,
and in the spirit of TDD I would like to use TLA+ assumptions to verify that domain model is
correct.

The next version of generator allows users to implement plugins to input definitions from external systems like Salesforce,
and in this case I encountered this problem due to number of fields on an interface.

I can constraint domain ranges to cardilality 1, and have the generated to to check assumptions in a separate run,
if the answers to questions a,b,c, above, is no,no,no.

NB; Comments on avoiding state space explosion problem, and problems due to specification code volume already tackled
can be found in

https://github.com/jarjuk/tla-sbuilder#manage-state-space-explosion-and-allow-scaling

BR,
Jukka