Quantification over sequences

50 views
Skip to first unread message

Zixian Cai

unread,
Sep 4, 2018, 6:39:05 PM9/4/18
to tla...@googlegroups.com
Hi,

I’m just wondering whether it is possible to have quantification over non-numerals.
For example, I would like to say, \E lst \in Seq(1..n): … or \E lst \in Seq(Nat): …

When I check it using TLC, it says “TLC encountered a non-enumerable quantifier bound”.

Sincerely,
Zixian

Stephan Merz

unread,
Sep 5, 2018, 2:23:53 AM9/5/18
to tla...@googlegroups.com
TLA+ allows you to write bounded quantification over arbitrary sets and your examples are perfectly legal TLA+, but as the error message indicates, TLC is restricted to quantification over finite sets. You may override operator definitions (in the Toolbox tab Advanced Options -> Definition Override) and write something like

Seq(S) <- UNION { [1 .. k -> S] : k \in 0 .. 3 }

to restrict to sequences of length at most 3. In the case where S itself is infinite (such as Nat in your second example), you'll want to override its definition in a similar way.

Of course, you have to think about what this change of semantics means for your specification.

Regards,
Stephan
> --
> 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.

Zixian Cai

unread,
Sep 10, 2018, 7:25:03 AM9/10/18
to tla...@googlegroups.com
I guess the error message could be phrased better, because given a finite set S, Seq(S) is enumerable.

Sincerely,
Zixian

Stephan Merz

unread,
Sep 10, 2018, 7:38:07 AM9/10/18
to tla...@googlegroups.com
The meaning of "enumerable" as used by TLC is explained in section 14.2.2 of Specifying Systems (p. 232). It is different from countable (sometimes called denumerable) sets in mathematics or recursively enumerable sets in computability.

Stephan

Zixian Cai

unread,
Sep 10, 2018, 8:01:41 AM9/10/18
to tla...@googlegroups.com
Hi Stephan,

Thanks for the explanation. it makes sense now.

Sincerely,
Zixian
Reply all
Reply to author
Forward
0 new messages