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.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.