[tlaplus] Re: Understand symmetric set

[Shiyao MA <i@xxxxxxxxx>]

To be specific. For the example,

CONSTANT Foos

\* ...

variables x \in Foos, y \in Foos;

begin

    print <<x, y>>;

end algorithm;

where Foos = {a, b} and declared symmetric.

Then only <<a, b>>, and <<a, a>> will be outputted.  but not <<b, b>>.

Why is that?

-- 
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.