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

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



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