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.