合金中的 A4options.symmetry 和签名实例排列

Question

我在 Alloy 中建模了一个图表转换链。我对求解结果的任何链感兴趣，但有些链是完全相同的。 除了签名实例之间的排列之外，它们是相同的，但实例之间的关系从一个解决方案到另一个解决方案形成完全相同的图。

有没有办法避免这些多余的解决方案？ 我在 A4Option 类中看到了一个对称选项，但我并不真正了解如何配置它。

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

如果我输入 0 是否意味着它被禁用？如果我设置更高的值，它会避免对称吗？ 如果您将一组原子和这些原子之间的关系视为一个图。 Ans邻接矩阵作为表征矩阵中原子之间的关系。 对称是否意味着 2 个实例具有等效的邻接矩阵？

为了降低求解复杂度，有没有办法向求解器指定我们对某些特定的签名实例排列或关系排列不感兴趣，而是对它们的架构配置感兴趣？

提前致谢。

Answer 1

如果我把 0 [对称破坏] 设置为禁用，这是否意味着？

是的

如果我设置一个更高的值，它会避免对称吗？

是的，尽力而为。

对称是否意味着两个实例具有等效的邻接矩阵？

我不知道你所说的“邻接矩阵”是什么意思，但无论如何，答案很可能是“不一定”。对称破坏只是一种启发式方法。它是在低于 Alloy AST 的级别上实现的，这意味着在您的域模型的高级别上有意义的一些对称性不一定会被 Alloy Analyzer 自动检测和破坏。

为了降低求解复杂度，有没有办法指定 我们对某些特定签名不感兴趣的求解器 实例排列或关系排列，但在它们的 架构配置？

我认为使用 Alloy 不容易做到这一点。