合金谓词树

Question

我试图用合金写一个谓词，它将确定一组节点是否是树。我有伪代码，但对如何实现它感到困惑。我是合金的新手，所以感谢所有提前做出回应的人。

sig Node[]

pred isTree [r: Node -> Node] {
// Every node reachable from root
// No cycles
// No node has more than 1 more parent.
}

Answer 1

你可以看看这个建模文件系统的online Alloy tutorial。它也是一个树形结构，所以你几乎得到了你的答案。

更具体的答案需要更具体的问题并显示您的尝试。

我们不会放弃家庭作业的解决方案;-)。