Dear Yuri,
TLC evaluates "assignments" q \in S (or q' \in S in an action definition) by enumerating the elements of S. When TLC says that the right side of \in is not enumerable, it actually means that it is infinite. In your case, that's because the set of sequences over any non-empty (even finite) set is infinite. See Section 14.2.2 of "Specifying Systems" for the details. In particular, TLC will also fail if you replace your definition by
BoundedSeq(Data, n) == { s \in Seq(Data) : Len(s) <= n } Init == q \in BoundedSeq(Data, 3)
although the set of possible initial values is now finite.
Regards, Stephan
TLC can check this spec:
EXTENDS Sequences
VARIABLE q
Init == q = <<1, 2, 3>>
Next ==
/\ q # <<>>
/\ q' = Tail(q)
Spec == Init /\ [][Next]_q
But when I add
CONSTANT Data and replace Init with Init == q \in Seq(Data)
TLC reports an error
In computing initial states, the right side of \IN is not enumerable.
line 7, col 9 to line 7, col 23 of module ConstantTest
The error occurred when TLC was evaluating the nested
expressions at the following positions:
The error call stack is empty.
Seq(Data) is defined as a set of all sequences of elements of set Data and q \in Seq(Data) says that q is an element of that set, which is a sequence. Could somebody help me understand what I am doing wrong when defining Init like q \in Seq(Data)? Thank you,
Yuri
--
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.
|