[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Understand symmetric set




Hi.

Symmetry should be the property between a set S and the _expression_ it is applied to.

So in the example, we have the set Foos = {a, b}.
And we have the usage: "variables x \in Foos, y \in Foos;"

I wonder, in what meaning, makes Foos being symmetry to the variable initialization.  For example, you mentioned <<b, b>> is equivalent to <<a,a>>, but why? and how is that related to symmetry?

Essentially, what defines symmetry?

Best,


On Monday, 25 March 2019 15:13:07 UTC+8, Stephan Merz wrote:
According to your declaration of symmetry, <<b,a>> is considered equivalent to <<a,b>>, and <<b,b>> is equivalent to <<a,a>>.

Stephan

On 25 Mar 2019, at 07:09, Shiyao MA <i...@xxxxxxxxx> wrote:

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+u...@googlegroups.com.
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+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.