Seq({"xxx"}) is not enumerable

[chin...@xxxxxxxxx]

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.