Re: [tlaplus] Quantification over sequences

[Stephan Merz <stepha...@xxxxxxxxx>]

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.