0

假设我有一个简单的模型如下： sig P{r:some P} sig Q{} run {} for 2 P, 2 Q

这里有谁知道合金如何生成对称破坏谓词以减少该模型的实例数量？

4

1 回答 1

3

Alloy 本身依赖于另一个名为 Kodkod 的关系模型查找器作为其后端。Kodkod 使用一种称为贪婪基础分区的技术生成对称破坏谓词，该技术在 Emina Torlak 的论文（第 3 章）中有详细说明：

http://people.csail.mit.edu/emina/pubs/kodkod.phd.pdf

于 2012-11-22T14:59:08.883 回答