Alloy Practice Problem: Ring

I probably should have done this first since it is an earlier exercise in the book.

The signature is again pretty simple

some sig Node { adjs: set Node }

To have a set of nodes form a ring each node must have exactly one successor

pred ring() {
  all n: Node | one n.adjs
}

Having exactly one successor doesn’t prevent disconnected loops though so we get stuff like the following

Not rings

The above satisifies all our conditions but clearly is not a ring so we need some other condition that specifies the connectdness of the ring. We can do that with the transitive closure. We’ll say that for any two distinct nodes each must be in the transitive closure of the other

pred ring() {
  all n: Node | one n.adjs
  all disj n, n': Node | n in n'.^adjs && n' in n.^adjs
}

Now when we run the model we get correct results

run ring for 5 Node

Correct ring