# Seq({"xxx"}) is not enumerable

Hi everyone,
I am a beginner in learning TLA.  I follow a example in the book which I got in Lamport's homepage,  and I got an error message while I am running model checker, the error message is something like this :
Attempted to enumerate { x \in S : p(x) } when S:

Seq({"xxx"})

is not enumerable

The error occurred when TLC was evaluating the nested

expressions at the following positions:

The error call stack is empty.

And this is my code:

VARIABLE q, event

CONSTANT N

CONSTANT msg

BoundedSeq(Data, n) == { s \in Seq(Data) : Len(s) <= n }

TypeInvariant ==   /\ q \in BoundedSeq(msg,N)

/\ event \in {"xx", "yy"}

Init == /\ Print("init q", TRUE)

/\ q = <<>>

/\ Print(q, TRUE)

ie == CHOOSE e:e \in event

enque ==  /\ Print(q, TRUE)

/\ (q' = Append(q, ie) => (Len(q) < N))

I assigned the constant msg with "msg <- {"xxx"}", when I run the model checker, I got an error posted above.

Actually, what I want to do is define a Sequence with length N, and each element of the Seq is "msg" who type is event. So what the efficient way of doing this?

Thanks very much.

All the best.