A4options.symmetry and signature instances permutattions in Alloy

Question

I have modeled a diagram transformation chain in Alloy. I am interested in any chain that results of the solving, but some of the chains are exactly the same. They are the same except permutation between signature instances, but the relations between instances form exactly the same graphs from one solution to an other.

Is there a way to avoid these redundant solutions? I saw a symmetry option in the A4Option class but I didn't really understand how to configure it.

    /** This option specifies the amount of symmetry breaking to do (when symmetry breaking isn't explicitly disabled).
 *
 * <p> If a formula is unsatisfiable, then in general, the higher this value,
 * the faster you finish the solving. But if this value is too high, it will instead slow down the solving.
 *
 * <p> If a formula is satisfiable, then in general, the lower this value, the faster you finish the solving.
 * Setting this value to 0 usually gives the fastest solve.
 *
 * <p> Default value is 20.
 */

Does it mean if I put 0 it is disabled? if I put a higher value does it avoid symmetry? If you consider a set of atoms and relations between these atoms as a graph. Ans an adjacency matrix as the characterization the relation between atoms in a matrix. Does symmetry means 2 instances that have equivalent adjacency matrix?

In order to reduce the solving complexity, is there a way to specify to the solver that we are not interested in some specific signature instances permutation or relation permutation but in their architecture configuration?

Thanks in advance.

Answer 1

Does it mean if I put 0 [symmetry breaking] is disabled?

Yes

if I put a higher value does it avoid symmetry?

Yes, the best it can.

Does symmetry means 2 instances that have equivalent adjacency matrix?

I don't know what you mean by "adjacency matrix", but in any case, the answer is likely to be "not necessarily". Symmetry breaking is just a heuristic; it is implemented at a level lower than the Alloy AST, meaning that some symmetries that make sense at a high level of your domain model are not necessarily automatically detected and broken by the Alloy Analyzer.

In order to reduce the solving complexity, is there a way to specify to the solver that we are not interested in some specific signature instances permutation or relation permutation but in their architecture configuration?

I don't think that can be readily done using Alloy.