alloy

How to visualize a graph having multiple edge types in Alloy


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

enter image description here

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?


Solution

  • 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 }