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

*From*: Y2i <yur...@xxxxxxxxx>*Date*: Mon, 29 Apr 2013 18:31:18 -0700 (PDT)*References*: <6ccc4957-05c0-4d92-bce0-f3038e29671b@googlegroups.com> <D3D65DA6-B6AE-4D93-B141-F6C229307D20@gmail.com> <ee0d1cfb-369a-42a6-8e56-180cf119b6cd@googlegroups.com> <cff4d4e3-a12e-4362-8863-db2acd819c8a@googlegroups.com> <f1e8d12c-50cf-48de-849f-892e552a034b@googlegroups.com>

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

**Follow-Ups**:

**References**:**In computing initial states, the right side of \IN is not enumerable***From:*Y2i

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

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

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

- Prev by Date:
**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable** - Next by Date:
**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable** - Previous by thread:
**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable** - Next by thread:
**Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable** - Index(es):