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

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

From: Dominik Hansen <do.han...@xxxxxxxxxxxxxx>
Date: Mon, 29 Apr 2013 01:54:50 -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>

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:
- Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable
  - From: Y2i

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

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):
- Date
- Thread