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