为何Alloy无法为简单树结构找到反例？

你的问题出在第二个fact的约束逻辑上，你构造的反例结构并不满足模型中的fact，所以Alloy不会生成该结构，自然找不到反例，这是理解误区而非Alloy的bug。

具体原因 #

看你定义的第二个fact：

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

• ^parent是parent关系的传递闭包，对于parent = none的节点（比如你构造的N1），i.^parent是空集，因此i.^parent.root也是空集。
• 但你的NonRoot中root字段定义为one Root，要求每个节点的root必须是一个非空的单元素Root集合。
• 空集和非空集不可能相等，因此所有parent = none的NonRoot节点都会被这个fact排除，你构造的N1根本不会出现在合法的模型实例中。

修正方案 #

把fact中的^parent换成*parent（自反传递闭包），*parent会包含节点自身，这样：

• 当节点没有父节点时，i.*parent就是节点自己，i.*parent.root等于i.root，等式自然成立；
• 当节点有父节点时，i.*parent包含所有祖先，保证节点的root和所有祖先的root一致，符合你原本的设计意图。

修正后的fact代码：

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

此时再运行check no_ancestry for 6，Alloy就能找到你预期的反例结构了。

内容的提问来源于stack exchange，提问作者typesanitizer