[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] In computing initial states, the right side of \IN is not enumerable

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.


On Apr 28, 2013, at 7:32 AM, Y2i <yur...@xxxxxxxxx> wrote:

TLC can check this spec:

EXTENDS Sequences
Init == q = <<1, 2, 3>>
Next ==
  /\ q # <<>>
  /\ q' = Tail(q)
Spec == Init /\ [][Next]_q

But when I add


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,

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.