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

Re: The effect of symmetry sets on TLC performance

Problem 2 does not exist for two reasons.  (1) While TLC fingerprints the permuted state, it computes next states based on the actual state.  Hence, every state that it examines is reachable.  (2) If your spec is actually symmetric, then every permutation of a reachable state is reachable.  If there are permutations that are not reachable, then your model is incorrect.  However, the result of this incorrectness is that TLC may fail to examine a reachable state that it should examine; it will not cause it to examine unreachable states.


On Wednesday, December 2, 2015 at 12:34:32 PM UTC-8, Ron Pressler wrote:
I've thought of the problem some more, and think I have more insight:

1. The current approach actually computes all permuted states from each reachable state by performing the permutations, but storing only a (deterministically) selected representative. This assumes that building such steps through permutations is faster than reaching it through a next step. The difference, however, is not as big as it can be, which can make this optimization not powerful enough or even somewhat harmful, and potentially very harmful in light of point 2.

2. It is possible (and is indeed the case in my model) that many of the permuted states -- while valid -- are not actually reachable. This means that the optimization computes many more states than would have been computed through reachability alone, and due to 1, it is sensitive to even to non-extreme correlations between symmetry sets. As an example, we can have two symmetry sets {a, b, c} and {x, y, z} that are both valid but are strongly correlated in the model which may ensure that in all reachable states, `a` always maps to `x`, `b` to `y` and `c` to `z`. Which means that the optimization will compute 9 steps, while only 3 are actually reachable (i.e. 3x states). As the computation via permutation is less than 3 times faster than computation via next-step, the result is a net loss which may be large.

Problem 1 may be solved through a different implementation of permute(), preferably one that doesn't allocate an actual complete state for each permutation.

Problem 2 may be solved by letting the user supply a predicate which would validate reachable compund permutations. In the example above, it would declare the compund permutation ([a |-> b, b |-> c, c |-> a], [x |-> y, y |-> z, z |->x]) as valid, but ([a |-> b, b |-> c, c |-> a], [x |-> x, y |-> y, z |->z]) as invalid.