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

Re: [tlaplus] The effect of symmetry sets on TLC performance

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