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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Thu, 3 Dec 2015 11:14:29 -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> <6e48bd0f-c441-44b3-893f-6acb6561cde4@googlegroups.com> <b57a9c90-24f3-430f-861e-5607438b46de@googlegroups.com>

If you look in Specifying Systems, you will see that you can specify

the kind of permutation set you want, if you run TLC from the command

line, by using the appropriate SYMMETRY statement in the cfg file.

the kind of permutation set you want, if you run TLC from the command

line, by using the appropriate SYMMETRY statement in the cfg file.

This flexibility could be the cause of the performance problem you

have discovered with symmetry. Given an arbitrary symmetry group, TLC

probably has to generate all permutations of the state to find the one

whose fingerprint it should use. It's possible that TLC does this

even for the symmetry groups obtained by declaring symmetry sets, even

though in this case there's a faster way to do it. We will look into

this.

have discovered with symmetry. Given an arbitrary symmetry group, TLC

probably has to generate all permutations of the state to find the one

whose fingerprint it should use. It's possible that TLC does this

even for the symmetry groups obtained by declaring symmetry sets, even

though in this case there's a faster way to do it. We will look into

this.

Leslie

On Thursday, December 3, 2015 at 10:09:31 AM UTC-8, Ron Pressler wrote:

Even if not symmetrical in both sets, it is surely symmetrical in {<<a, x>>, <<b, y>>, <<c, z>>}, because the original model (just `foo`) is symmetrical in {x, y, z}, no? Perhaps TLC should provide a way to specify this symmetry (e.g. with a predicate on composed permutations)?Ron

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

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

**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:
**TLA+ logic** - Previous by thread:
**Re: [tlaplus] The effect of symmetry sets on TLC performance** - Next by thread:
**TLA+ Toolbox nightly: Periodic workspace save java.lang.NumberFormatException** - Index(es):