Though Alloy has a graph module, the module does not distinguish different edge types.
I make a graph having multiple edge types in Alloy. But the visualization is against intuition.
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
The problem with the visualization is that it connects nodes to edges, but intuitively, we want to see nodes connect to nodes.
Though I could change the to : Node -> lone Edge to to : Edge -> Node, but then it seems impossible to write the acyclicity constraint in a transitive way.
Is there better ways to do this?


One way to solve this issue, when using
to : Edge -> Node(or better:to : Edge lone -> Node), is to consider a binary relation between nodes that contains all pairs of connected nodes, regardless of the edge type. Then, in the Visualizer, you can hidetoand showedges. The acyclicity condition is also easier to write: