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 に答える