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 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