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

以获得相同的效果。