如何在Alloy中可视化多Edge类型图并兼顾无环约束？

调整模型结构，让Edge直接关联起始和终止节点，同时保留节点与出边的关联，既满足可视化需求，又能简洁编写无环约束：

sig Node {
  outEdges: set Edge  // 存储节点的所有出边
}

abstract sig Edge {
  start: one Node,  // 边的起始节点
  end: one Node     // 边的终止节点
}
sig VisibleEdge, HiddenEdge extends Edge {}

fact {
  // 确保边的起始节点正确关联该边
  all e: Edge | e in e.start.outEdges
  // 无环约束：节点无法通过边的传递关系回到自身
  all n: Node | n not in n.^(end.~start)
  // 所有边都属于某个节点的出边（避免孤立边）
  all e: Edge | e in Node.outEdges
  // 限制每种边最多一条
  lone VisibleEdge
  lone HiddenEdge
}

run {#outEdges > 2} for 5

核心说明 #

1. 可视化优化：通过Edge的start和end字段直接关联节点，Alloy可视化会自动渲染节点间的连接边，符合“节点直接相连”的直观需求，无需额外配置。
2. 无环约束实现：end.~start表示从节点到节点的直接可达关系（即通过一条边从A到B），^取其传递闭包后，判断节点不在自身的可达集合中，即可保证图的无环性。
3. 边的完整性：通过all e: Edge | e in e.start.outEdges和all e: Edge | e in Node.outEdges确保所有边都正确归属到起始节点，避免出现孤立的边实例。

内容的提问来源于stack exchange，提问作者luomein