如何可视化合金中具有多种边类型的图

Question

虽然 Alloy 有图模块，但该模块不区分不同的边类型。

我在 Alloy 中制作了一个具有多种边缘类型的图表。但可视化与直觉相反。

sig Node { to : Node -> lone Edge}

abstract sig Edge {}
sig VisibleEdge , HiddenEdge extends Edge{}

fact{
all n : Node | not n in n.^(to.Edge) // acyclicity
all e : Edge  | e in Node.(Node.to)
lone VisibleEdge 
lone HiddenEdge
}

run {#to > 2 } for 5

可视化的问题在于它将节点连接到边缘，但直观上，我们希望看到节点连接到节点。

虽然我可以将

to : Node -> lone Edge

更改为

to : Edge -> Node

，但似乎不可能以传递的方式编写非循环约束。

有更好的方法吗？

Answer 1

解决此问题的一种方法是，在使用

to : Edge -> Node

（或更好：

to : Edge lone -> Node

）时，考虑包含所有连接节点对的节点之间的二元关系，无论边类型如何。然后，在可视化工具中，您可以隐藏

to

并显示

edges

。非循环条件也更容易写：

fun edges : Node -> Node { { n1, n2: Node | some n1.to.n2 } }
fact { all n : Node | n not in n.^edges }