This spec creates very few connects, is that plausible? I'm attempting exercise A.2.1 from the book http://alloytools.org/book.html. Having got this far, I find that when stepping through instances I only ever get 2 connects links, no matter how many requests links, when using the MiniSat solver. When using MiniSat plus Unsat core, I sometimes get more connects, but not many requests. Obviously, these all satisfy the model, but it feels wrong to me. Am I over-thinking this?
module exercises/telephone

sig Phone {
    , requests : set Phone
    , connects: lone Phone
} 

fact minimum_system {
    some requests
    some connects
}

fact dont_call_yourself {
  no p: Phone | p.connects = p
  no p: Phone | p in p.requests
}

fact connect_from_a_request {
    no (connects - requests)
}

fact only_receive_once {
    all p: Phone.connects | one ~connects[p]
}

fact receiver_or_caller_only {
    no (Phone.connects &amp; Phone.~connects)
}

pred show {}

run show for exactly 12 Phone
When you get lots of instances, it's not really practical to look through them all. What most Alloy users would do in this case is to add a constraint to the show predicate to see if you can get the instance you expect. So I modified it to
pred show {
#connects &gt; 4
#requests &gt; 4
}

and now I see instances with more than 4 connects and requests.
Another suggestion: don't use exactly unless you really need to. You usually want to look for all instances up to some bound, and if you set it to exactly, you might find that you get no instances because it's not possible to construct one with exactly that number. For example, if you don't allow conference calls and you require phones to matched one to one, and you then set the bound to &quot;exactly 3&quot; you would get no solutions.