Attempted to construct a set with too many elements (>1000000).
jarjuk
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
Leslie Lamport
As you must realize, you have defined t_salesf_Lead to be a set with
about 2^50 elements. TLC cannot enumerate the elements of such a big
set. It can be hard to use a set in a spec in such a way that TLC
doesn't have to enumerate it. You can ensure that TLC doesn't have to
enumerate the set S by not defining S, and instead defining an
operator InS where InS(x) is true iff x \in S.
In your example, you can define the following, where I have
abbreviated t_salesf_Lead as TSFL.
TSFL_Domains ==
[ Id |-> d_lead_id,
IsDeleted |-> d_not_used,
MasterRecordId |-> d_not_used,
... ]
TSFL_Fields == DOMAIN TSFL_Domains
InTSFL(x) ==
/\ DOMAIN x = TSFL_Fields
/\ \A f \in TSFL_Fields :
x[f] \in TSFL_Domains[f]
(Note: If you want to write proofs, you'll need to add to the
definition of InTSFL(x) a conjunction asserting that x is a function.
However, this definition works for TLC because TLC will report an
error in evaluating InTSFL(e) if e is not a function.)
If you can write your spec using InTSFL rather than TSFL, then this
will solve your problem. Otherwise, you will not be able to use TLC
to check the spec.
Leslie
jarjuk
I will take take a look at my spec, and how it can be modified using the example below.
Jukka
On Monday, April 25, 2016 at 7:23:44 PM UTC+3, Leslie Lamport wrote:
TSFL_Fields == DOMAIN TSFL_Domains
InTSFL(x) ==
/\ DOMAIN x = TSFL_Fields
/\ \A f \in TSFL_Fields :
x[f] \in TSFL_Domains[f]
If you can write your spec using InTSFL rather than TSFL, then this
will solve your problem. Otherwise, you will not be able to use TLC
to check the spec.
Leslie