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

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

Thank you for instructions!

I will take take a look at my spec, and how it can be modified  using the example below.


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.