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.