Why does Alloy not find a counter-example for a simple tree structure?

Question

Here is a minimized Alloy model I tested with Alloy 6.1.0 on macOS:

sig Root {}

sig NonRoot {
  root : one Root,
  parent : lone NonRoot
}

fact acyclic {
  no i : NonRoot | i in i.^parent
}

fact root_consistent_with_ancestors {
  all i : NonRoot
  | i.root = i.^parent.root
}

assert no_ancestry {
  no disj nr1, nr2 : NonRoot
  | nr1.parent = nr2
}

check no_ancestry for 6

It seems like Alloy should be able to find a small counter example to this with the following structure:

• 1 root node R
• 1 non-root node N1 with root = { R } and parent = none
• 1 non-root node N2 with root = { R } and parent = { N1 }.

Am I misunderstanding something or is this an Alloy bug?

Answer 1

The problem is that this fact is too constraining:

fact root_consistent_with_ancestors {
  all i : NonRoot
  | i.root = i.^parent.root
}

For the case of the first child of the root which doesn't have a parent, i.^parent.root is the empty set. However, i.root is a singleton set.

As a consequence, Alloy will not generate any NonRoot elements at all.

This can be tested by removing the check and generating examples using:

pred example {}
run example for 3

You'll see that only Root nodes are being generated.

One way to fix the model is to use i.parent = none or i.root = i.^parent.root. That gives the desired result.