[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

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.