Hello,you did not show the actual TLA+ module that you are using, and the parts that you show contain several problems, so I am not sure if I can give you a satisfactory answer.To understand TLC's error message, it is important to keep in mind that TLC can only evaluate sets that it can syntactically determine to be finite. For example, althoughBoundedSeq({"xxx"}, 1) = { << >>, << "xxx" >> }is clearly a finite set, if you write an _expression_ such as\E seq \in BoundedSeq({"xxx"}, 1) : ...TLC expands the definition of BoundedSeq, which refers to Seq({"xxx"}), and this is an infinite set (it contains sequences of unbounded length), so TLC gives up evaluation with the error message that you indicate.However, in the part of your specification that you copied into the message, BoundedSeq occurs only in the typing invariant in the formq \in BoundedSeq(msg, N)and TLC should be able to evaluate this _expression_. You can find more information about this topic in section 14.2.2 of Specifying Systems.If you cannot avoid expressions that TLC refuses to evaluate because they involve infinite sets, there is an option to override built-in constructors, for example you could writeSeq(S) <- UNION { [1 .. n -> S] : n \in 0 .. N }(or directly override your definition of BoundedSeq). However, this must be used with care since you can easily introduce errors in your model.––––Other problems in the part of the specification that you show are:- Init does not initialize the variable event.- The action enque does not make sense as it is written (presumably the implication should be a conjunction), and again it does not determine the value of variable event'.–––––As a beginner's introduction to TLA+, I suggest that you look at the Hyperbook [1] and/or follow the video courses [2] that Leslie puts online.Hope this helps,StephanOn 2 Jun 2017, at 01:40, chi...@xxxxxxxxx wrote: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.
--
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...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus .
For more options, visit https://groups.google.com/d/optout .