| Hi,
model checking modulo symmetry is explained in section 14.3.4 of Specifying Systems. By declaring the set Foos = {a,b} as a symmetry set, you assert that for any permutation p : Foos -> Foos, the states s and p(s) are considered equivalent, where p(s) is obtained from s by replacing every value v in Foos by p(v).
In particular, consider the permutation that maps a to b and b to a and the state s where s(x) = a and s(y) = a, then p(s) maps both variables to b. If TLC has already encountered state s (and therefore output <<a,a>>) and later encounters state p(s), it will consider the latter as a state that it has already seen. That's why the output <<b,b>> is not produced.
Does this clarify your question? Note in particular that if you declare Foo as a symmetry set, TLC does not check if the specification is indeed symmetric with respect to the permutations of set Foo. If it isn't, all bets are off with respect to the verdict that TLC produces.
Stephan On 26 Mar 2019, at 03:13, Shiyao MA < i@xxxxxxxxx> wrote:
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
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...@googlegroups.com. 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.
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.
|