Find centralized, trusted content and collaborate around the technologies you use most.
Teams
Q&A for work
Connect and share knowledge within a single location that is structured and easy to search.
次のような単純なモデルがあるとします: sig P{r:some P} sig Q{} run {} for 2 P, 2 Q
このモデルのインスタンス数を減らすために、合金が対称性を破る述語を生成する方法を知っている人はいますか?
Alloy 自体は、バックエンドとして Kodkod と呼ばれる別のリレーショナル モデル ファインダーに依存しています。Kodkod は、Emina Torlak の論文 (第 3 章) で詳述されている貪欲なベース パーティショニングと呼ばれる手法を使用して、対称性を破る述語を生成します。
http://people.csail.mit.edu/emina/pubs/kodkod.phd.pdf