Re: [tlaplus] Symmetry sets

[Philip White <philip@xxxxxxxxxxxxx>]

I see… yes, I was expecting TLC to try all selections. Thank you very much for clarifying this newbie mistake.

What I like about CHOOSE is that it will select exactly one item, or give a model error if it couldn’t find one. With the second (symmetric) syntax you suggest, we get a set, and the set may be empty. To make up for CHOOSE’s functionality, is using a type invariant the answer?

Philip


> On Feb 14, 2019, at 12:18 PM, Hillel Wayne <hwayne@xxxxxxxxx> wrote:
> 
> Hi Philip,
> 
> It sounds like there might be an XY problem here. CHOOSE is consistent: for the same set and predicate, it will choose the same element across all behaviors. If you're expecting TLC to try all selections, this could lead to your spec passing when you think it should fail. This is a common pitfall for beginners, which is why I'm bringing it up now.
> 
> If this is an issue in your spec, you can replace
> 
> item' = CHOOSE x \in Set: P(x)
> 
> with
> 
> item' \in {x \in Set: P(x)}
> 
> which retains symmetry.
> 
> H

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.