Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable

[Y2i <yur...@xxxxxxxxx>]

Dear Dominik,

I realized that a record or a tuple is a shortcut for a function but did not think that a function with domain 1..n can be treated as a sequence.  This is a very cleaver technique, thank you for sharing it!

And what about using { [x -> d] : x \in {1..y : y \in 0..n} } instead of { [x -> d] : x \in 1..n }?  Was it in order to take into account sequences of length 0?

Thank you again,

Yuri

On Monday, April 29, 2013 1:54:50 AM UTC-7, Dominik Hansen wrote:

Dear Yuri,

in TLA+ a sequence of length n is a function with the Domain 1..n .Hence [1..n -> Data] defines the set of all sequences of length n.

The UNION-operator is used to collect all sequences of different length (from 0 to n) in a set.

Dominik