CODEWITHSUNDEEP
logicalloymodel-checking
erik
erik

Reputation: 3880

Modeling a completely connected graph in Alloy

I'm trying to get my feet wet with Alloy (also relatively new-ish to formal logic as well), and I'm trying to start with a completely connected graph of nodes.

sig Node {
  adj : set Node
}

fact {
  adj = ~adj    -- symmetrical
  no iden & adj     -- no loops
  all n : Node | Node in n.*adj -- connected
}

pred ex { }
run ex for exactly 3 Node

As you can see from the image, Nodes 0 and 1 aren't connected. I thought that my fact was enough to make it completely connected...but perhaps I missed something.

Alloy

Upvotes: 3

Views: 853

Answers (1)

Aleksandar Milicevic
Aleksandar Milicevic

Reputation: 3857

How about

adj = Node -> Node - iden

This basically says that adj contains all possible pairs of nodes, except identities (self-loops).

The reason why it is ok that Node1 and Node2 are not connected for your model is the last clause of your fact which constrains that for each node, all nodes are transitively reachable, but it seems to me that you want them to be immediately reachable. Alternatively to using my solution above, you can change

all n: Node | Node in n.*adj to all n: Node | (Node - n) in n.adj

to get the same effect.

Upvotes: 4

Related Questions