Alloy 和 Kodkod 中总排序的优化

Question

据说在很多地方（例如这里 or there）为了提高分析效率（并让原子名称出现在"natural"中，总序关系是硬连线的命令）。

据我了解，优化是在 Kodkod (in this piece of code) 中进行的。然而，是否有一篇文章或文档解释得更详细（比 Java 文档，它用布尔矩阵的方式说话并且没有提供算法的论证——这在源代码文档中很好——） Kodkod 中的优化？据我所知，E. Torlak 的博士论文没有谈到这些（I. Shlyakhter 的一篇论文谈到了其他优化，但我不知道这些是在 Kodkod 还是 Alloy 中实现的）。

Answer 1

此优化是在您找到的代码位置的 Kodkod 中进行的。 Ilya Shlyakhter's PhD thesis（第 111 页，第 4.5.5 节）对其进行了简要描述。