While learning Alloy this was one of the exercises in the book I was reading. It’s kinda weird to combine “acyclic” and “undirected” for graphs but there is a way to formalize the intuition about what it means for an undirected graph to be acyclic.

For everything that follows I’m going to assume that you understand the Alloy syntax and semantics. If not then I recommend some posts I wrote for beginners to get started over at dev.to: 1, 2, 3, 4, 5.

The graph structure is expressed in terms of nodes. The node signature is pretty simple and just says a node can be connected to 0 or more other nodes

1 2 |
open util/relation some sig Node { adjs: set Node } |

Next we need to specify the conditions for making the graph undirected and we do that by forcing the `adjs`

to be symmetric

1 2 3 |
pred acyclic() { adjs = ~adjs } |

If that’s all we did we’d get a lot more than just “acyclic” undirected graphs so we need to set up a few more restrictions. We don’t want any self loops so we make sure that’s the case

1 2 3 |
fact { all n: Node | (n -> n) not in adjs } |

We also want to rule out trivial graphs

1 |
fact { all n: Node | n in dom[adjs] } |

The above fact forces all nodes to participate in the `adjs`

relation because we don’t want disconnected graphs with nodes just hanging out. If you run the model at this point you’ll get some interesting results

We want to rule out those cases but it is not obvious how to do that. If you stare at the above “cyclic” undirected graphs a thought might occur to you: why not treat the graph as a directed graph and then try to figure out what the acyclicity condition would look like?

If you look at the smallest example with 3 nodes you’ll notice there is a cycle starting at `Node$0`

and the cycle is `Node$0 -> Node$1 -> Node$2 -> Node$0`

and we want to rule that out. There is an obvious way to break the cycle and it’s removing one of the edges. We are going to build our definition of acyclicity on this intuition.

If you look at any node and remove the edge connecting that node to it’s neighbor then the cycle is broken. Another way of specifying the condition is to say if we look at any two nodes that are connected then if we remove one of the edges going back then we should not be able to get back to where we started

1 2 3 4 |
pred acyclic() { adjs = ~adjs all disj n, n': Node | (n -> n') in adjs => n not in n'.^(adjs - (n' -> n)) } |

Running the model with the above conditions will give the correct results

1 |
run acyclic for 5 Node |

If you find a better way then let me know.