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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 3 Dec 2015 09:43:38 -0800 (PST)*References*: <feb1173e-380c-4cb1-80ac-a5d8edf1c108@googlegroups.com> <0d9ae6b0-f5f1-4159-a933-32921111ab3d@googlegroups.com> <c7f7df3e-118a-42e1-aca4-e7a47dced84c@googlegroups.com> <82111398-b195-40c1-8926-59e179145fa6@googlegroups.com> <f283857c-31a1-4d9b-b22a-c39fd47f0c44@googlegroups.com> <4c9e536c-f18f-4b99-adad-7ffa3a4b38aa@googlegroups.com> <9a1e660e-f417-4413-814a-f1f127afcaf4@googlegroups.com> <EC355E14-A73D-4C02-A723-D4A83EBA503E@cs.uni-duesseldorf.de> <655e0ddb-9391-4f5e-915e-c241ab7aa6cb@googlegroups.com>

I think this model is semantically symmetrical in both sets

If you are convinced that the model of the spec is symmetrical, then

you should be able to prove that it satisfies the definition of

symmetry.

you should be able to prove that it satisfies the definition of

symmetry.

Thank you for making me realize that symmetry with respect to a set S

can be broken by CHOOSE expressions involving S other than ones of the

form CHOOSE x \in S : ... -- for example a CHOOSE _expression_ like

can be broken by CHOOSE expressions involving S other than ones of the

form CHOOSE x \in S : ... -- for example a CHOOSE _expression_ like

Map == CHOOSE f \in [S -> T] : ...

As I did mention, symmetry can also be broken by instantiating a

constant like Map with an _expression_ that explicitly mentions

individual elements of S.

constant like Map with an _expression_ that explicitly mentions

individual elements of S.

Leslie

**Follow-Ups**:**Re: [tlaplus] The effect of symmetry sets on TLC performance***From:*Ron Pressler

**References**:**The effect of symmetry sets on TLC performance***From:*Ron Pressler

**Re: The effect of symmetry sets on TLC performance***From:*Ron Pressler

**Re: The effect of symmetry sets on TLC performance***From:*Leslie Lamport

**Re: The effect of symmetry sets on TLC performance***From:*Ron Pressler

**Re: The effect of symmetry sets on TLC performance***From:*Leslie Lamport

**Re: The effect of symmetry sets on TLC performance***From:*Ron Pressler

**Re: The effect of symmetry sets on TLC performance***From:*Ron Pressler

**Re: [tlaplus] The effect of symmetry sets on TLC performance***From:*Michael Leuschel

**Re: [tlaplus] The effect of symmetry sets on TLC performance***From:*Ron Pressler

- Prev by Date:
**Re: [tlaplus] The effect of symmetry sets on TLC performance** - Next by Date:
**Re: [tlaplus] The effect of symmetry sets on TLC performance** - Previous by thread:
**Re: [tlaplus] The effect of symmetry sets on TLC performance** - Next by thread:
**Re: [tlaplus] The effect of symmetry sets on TLC performance** - Index(es):