logic - Alloyでの完全連結グラフのモデリング

Question

私はAlloyで足を濡らそうとしています（これも比較的新しいもので、正式なロジックでもあります）。また、ノードの完全に接続されたグラフから始めようとしています。

sig Node {
  adj : set Node
}

fact {
  adj = ~adj    -- symmetrical
  no iden & adj     -- no loops
  all n : Node | Node in n.*adj -- connected
}

pred ex { }
run ex for exactly 3 Node

画像からわかるように、ノード0と1は接続されていません。私の事実はそれを完全に接続するのに十分だと思いました...しかし、おそらく私は何かを逃しました。

Answer 1

どうですか

adj = Node -> Node - iden

これは基本的にadj、アイデンティティ（自己ループ）を除いて、ノードの可能なすべてのペアが含まれていることを示しています。

Node1モデルに接続されていなくても問題ない理由Node2は、各ノードについてすべてのノードが推移的に到達可能であることを制約する事実の最後の節ですが、すぐに到達可能にしたいと考えています。上記の私のソリューションを使用する代わりに、変更することができます

all n: Node | Node in n.*adjにall n: Node | (Node - n) in n.adj

同じ効果を得るために。