合金：檢查與謂語樹關係

不知道如何描述的形式的樹關係：合金：檢查與謂語樹關係

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

合金：檢查與謂語樹關係

回答

相關問題