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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 25 Apr 2016 09:23:44 -0700 (PDT)*References*: <6bd6577b-f4ba-48ce-922a-c789c1dfa16b@googlegroups.com>

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

**Follow-Ups**:

**References**:

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