How to visualize a graph having multiple edge types in Alloy

50 views Asked by At

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?

2

There are 2 answers

2
Grayswandyr On BEST ANSWER

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 }
0
luomein On

Based on @Grayswandyr's answer, I updated my code as following,

sig Node { 
to : Edge lone ->  Node
}

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

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

fact{
//all n : Node | not n in n.^(to.Edge) // acyclicity
all e : Edge  | #(e.(Node.to)) = 1
}

run {#to > 2 } for 5

The visualization now is as expected.

enter image description here