| 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, although BoundedSeq({"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 form q \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 write Seq(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, Stephan
|