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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 30 Mar 2019 17:35:02 +0100*References*: <70a36d70-07a3-4afa-becf-a56016cb1dcf@googlegroups.com> <0b91e364-d3cf-4814-8d0c-6eb9049f328d@googlegroups.com> <D0A46015-F57A-46A5-A1B2-89CAA4F3151A@gmail.com> <552b5b73-3499-4581-86b8-a94fa2746c34@googlegroups.com>

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

**References**:**[tlaplus] Re: Understand symmetric set***From:*Shiyao MA

**Re: [tlaplus] Re: Understand symmetric set***From:*Stephan Merz

**Re: [tlaplus] Re: Understand symmetric set***From:*Shiyao MA

- Prev by Date:
**Re: [tlaplus] Why does adding a new step collapse my model to a single state?** - Next by Date:
**Re: [tlaplus] Re: Why is this temporal property violated?** - Previous by thread:
**Re: [tlaplus] Re: Understand symmetric set** - Next by thread:
**[tlaplus] Proving false with fairness** - Index(es):