# In computing initial states, the right side of \IN is not enumerable

TLC can check this spec:

EXTENDS Sequences
VARIABLE q
Init == q = <<1, 2, 3>>
Next ==
/\ q # <<>>
/\ q' = Tail(q)
Spec == Init /\ [][Next]_q

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 ConstantTest
The error occurred when TLC was evaluating the nested
expressions 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: