为什么 Alloy 没有找到简单树结构的反例？

【问题标题】：Why does Alloy not find a counter-example for a simple tree structure?为什么 Alloy 没有找到简单树结构的反例？
【发布时间】：2022-07-25 04:18:15
【问题描述】：

这是我在 macOS 上使用 Alloy 6.1.0 测试的最小化 Alloy 模型：

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

Alloy 似乎应该能够找到一个具有以下结构的小型反例：

1个根节点R
1 个非根节点 N1 与 root = { R } 和 parent = none
1 个具有root = { R } 和parent = { N1 } 的非根节点N2。

我是不是误会了什么，或者这是一个合金错误？

【问题讨论】：

标签： alloy

【解决方案1】：

问题是这个fact太受约束了：

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

对于没有父节点的根的第一个子节点，i.^parent.root 是空集。但是，i.root 是一个单例集。

因此，Alloy 根本不会生成任何 NonRoot 元素。

这可以通过删除check 并使用以下方法生成示例来测试：

pred example {}
run example for 3

您会看到只有Root 节点正在生成。

修复模型的一种方法是使用i.parent = none or i.root = i.^parent.root。这给出了预期的结果。

【讨论】：