树的合金谓词

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，其中对文件系统进行了建模。 它也是一个树形结构，所以你几乎有你的答案。

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

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