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 hide to
and show edges
. The acyclicity condition is also easier to write:
fun edges : Node -> Node { { n1, n2: Node | some n1.to.n2 } }
fact { all n : Node | n not in n.^edges }