합금 : 나는 경우</p> <pre><code>module tree pred isTree (r: univ −> univ) {...} run isTree for 4 </code></pre> <p>: 술어 트리 관계를 확인

방법의 형태로 나무의 관계를 설명하는 방법 궁금 내가 어떻게 위의 제약을 궁금합금 : 나는 경우</p> <pre><code>module tree pred isTree (r: univ −> univ) {...} run isTree for 4 </code></pre> <p>: 술어 트리 관계를 확인

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

합금 : 나는 경우</p> <pre><code>module tree pred isTree (r: univ −> univ) {...} run isTree for 4 </code></pre> <p>: 술어 트리 관계를 확인

답변

관련 문제