Re: [tlaplus] Quantification over sequences

[Zixian Cai <fzcz...@xxxxxxxxx>]

I guess the error message could be phrased better, because given a finite set S, Seq(S) is enumerable.

Sincerely,
Zixian

> On 5 Sep 2018, at 16:23, Stephan Merz <stepha...@xxxxxxxxx> wrote:
> 
> 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
> 
> 
>> On 5 Sep 2018, at 00:38, Zixian Cai <fzcz...@xxxxxxxxx> wrote:
>> 
>> 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
>> 
>> -- 
>> 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 https://groups.google.com/group/tlaplus.
>> For more options, visit https://groups.google.com/d/optout.
> 
> -- 
> 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 https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.