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

*From*: jarjuk <jar...@xxxxxxxxx>*Date*: Mon, 25 Apr 2016 11:43:09 -0700 (PDT)*References*: <6bd6577b-f4ba-48ce-922a-c789c1dfa16b@googlegroups.com> <f9b4d7f9-4ee0-4c9b-9f92-21f657e76124@googlegroups.com>

Thank you for instructions!

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:

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

**References**:**Attempted to construct a set with too many elements (>1000000).***From:*jarjuk

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

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