【发布时间】：2012-11-21 16:01:05
【问题描述】：
假设我有一个简单的模型如下： sig P{r:一些 P} 信号 Q{} 为 2 P、2 Q 运行 {}
这里有人知道合金如何生成对称破坏谓词以减少此模型的实例数量吗？
【问题讨论】：
标签： alloy
【发布时间】：2012-11-21 16:01:05
【问题描述】：
Alloy 本身依赖另一个名为 Kodkod 的关系模型查找器作为其后端。 Kodkod 使用一种称为贪心基划分的技术生成对称破坏谓词，该技术在 Emina Torlak 的论文（第 3 章）中有详细说明：
【讨论】：
-
好吧，假设你有关系常数 e1 和 e2，它们捕获了 a1 和 a2 上的关系，对称性是 (a1,a2)。我知道a1和a2之间可以打破对称性，但是关系常数e1和e2呢，那里有对称性，那你怎么能打破这种对称性呢？