在Alloy中建模完全连接的图 [英] Modeling a completely connected graph in Alloy

问题描述

我正在尝试着用Alloy(也对形式逻辑来说也相对较新)弄湿自己的脚，并且我试图从一个完全连接的节点图开始.

I'm trying to get my feet wet with Alloy (also relatively new-ish to formal logic as well), and I'm trying to start with a completely connected graph of nodes.

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没有连接.我以为我的事实足以使它完全连接起来……但是也许我错过了一些东西.

As you can see from the image, Nodes 0 and 1 aren't connected. I thought that my fact was enough to make it completely connected...but perhaps I missed something.

推荐答案

如何

adj = Node -> Node - iden

这基本上表示adj包含除身份(自循环)之外的所有可能的节点对.

This basically says that adj contains all possible pairs of nodes, except identities (self-loops).

对于您的模型而言，可以不连接Node1和Node2的原因是事实的最后一个子句，该子句约束每个节点的所有节点都可传递地到达，但在我看来，您希望他们能够立即到达.除了使用上述解决方案外，您还可以更改

The reason why it is ok that Node1 and Node2 are not connected for your model is the last clause of your fact which constrains that for each node, all nodes are transitively reachable, but it seems to me that you want them to be immediately reachable. Alternatively to using my solution above, you can change

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

以获得相同的效果.

这篇关于在Alloy中建模完全连接的图的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！