合金：检查与谓语树关系

不知道如何描述的形式的树关系：合金：检查与谓语树关系

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来建模。

非常感谢你提前！

来源

2016-09-07 Ellie A.

由于您已经省略了代码的一些细节，在假设所有谓词都正确的情况下，给定的代码应该确实描述了Node实例上的树结构。请注意，这是在宇宙中的所有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，因为表示不允许它，通过建设。

来源

2016-09-08 05:43:33 ivcha

我看到你有兴趣检查一个关系是否以通用的方式满足树的约束条件，也就是说，与关系的类型无关。

这是可能的合金，诀窍是，对于任何关系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 
    } 
}

第一个约束是用于可达性，第二个用于acyclicness和第三，以防止一个节点从具有多个父。

来源

2016-09-08 07:12:04

合金：检查与谓语树关系

回答

相关问题