Alloy：检查与谓词的树关系答案

【问题标题】：Alloy: checking a tree relationship with a predicateAlloy：检查与谓词的树关系
【发布时间】：2016-09-07 01:51:30
【问题描述】：

想知道如何以以下形式描述树关系：

module tree
pred isTree (r: univ −> univ) {...} run isTree for 4

如果我有：

refines module Graph
pred isConnected {
some n: Node |
(Graph.nodes = n) || (Graph.nodes = n.^(edges.(src + dest)))
}
pred noCycles {
all n: Node | n not in (n.^(outEdges.dest) + n.^(inEdges.src))
}
pred loneParent {
all n: Node | lone n.inEdges
}
fact isTree {
noDoubleEdges && isConnected && noCycles && loneParent
}

我想知道如何用 r: univ -> univ 对树上的上述约束进行建模。

非常感谢您！

【问题讨论】：

标签： tree relational alloy calculus

【解决方案1】：

我看到您有兴趣检查关系是否以通用方式满足树的约束，即独立于关系的类型。

这在 Alloy 中是可能的，诀窍是对于任何关系 r: univ->univ，r.univ 会给你关系的域，univ.r 会给你关系的范围（从中你可以得到所有关系所涉及的节点）。

您正在寻找的谓词是：

pred isTree (r: univ -> univ) {
     let nodes=univ.r + r.univ{
        one root : nodes | nodes = root.*r
        no n :nodes | n in n.^r 
        all n:nodes | lone n.~r
    }
}

第一个约束是可达性的，第二个是非循环性的，第三个是防止节点拥有多个父节点。

【讨论】：

【解决方案2】：

由于您省略了代码的一些细节，假设所有谓词都是正确的，给定的代码确实应该描述Node 实例的树结构。请注意，这是在 Universe 中的所有 Node 实例上完成的，仅根据 isTree 的事实，因此不需要额外的谓词。

请注意，虽然您的代码假定节点（以及整个树）在全局范围内，但根据给定参数定义定义有效树的谓词可能更方便，例如对于非周期性：

pred acyclicity [root: Node, tree: Node -> Node] {
    no ^tree & iden
}

在这种情况下，树是用根注释和定义父子关系的关系来定义的。之后，为了定义（将模型约束为）一棵有效的树，可以写一些类似于

pred isTree [root: Node, tree: Node -> Node] {
    reachability[root, tree]
    acyclicity[root, tree]
    loneParent[root, tree]
}

请注意，在这种情况下，您可能不需要对约束 noDoubleEdges 建模，因为通过构造表示不允许这样做。

【讨论】：