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

*From*: jarjuk <jar...@xxxxxxxxx>*Date*: Mon, 25 Apr 2016 02:01:39 -0700 (PDT)

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

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

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

**Follow-Ups**:**Re: Attempted to construct a set with too many elements (>1000000).***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Very simple question by TLA newcomer** - Next by Date:
**Re: Why Amazon Chose TLA+** - Previous by thread:
**Re: Very simple question by TLA newcomer** - Next by thread:
**Re: Attempted to construct a set with too many elements (>1000000).** - Index(es):