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

*From*: Y2i <yur...@xxxxxxxxx>*Date*: Sat, 27 Apr 2013 22:32:26 -0700 (PDT)

TLC can check this spec:

EXTENDS Sequences

VARIABLE q

Init == q = <<1, 2, 3>>

Next ==

/\ q # <<>>

/\ q' = Tail(q)

Spec == Init /\ [][Next]_q

But when I add

CONSTANT Data

and replace Init with

Init == q \in Seq(Data)

TLC reports an error

*In computing initial states, the right side of \IN is not enumerable.line 7, col 9 to line 7, col 23 of module ConstantTestThe error occurred when TLC was evaluating the nestedexpressions at the following positions: The error call stack is empty.*

Seq(Data) is defined as a set of all sequences of elements of set Data and q \in Seq(Data) says that q is an element of that set, which is a sequence.

Could somebody help me understand what I am doing wrong when defining Init like **q \in Seq(Data)**?

Thank you,

Yuri

**Follow-Ups**:

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