Alloy: проверка дерева отношений с помощью предиката

Question

Интересно, как описать древовидные отношения в виде:

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.

Огромное спасибо заранее!

Answer 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
    }
}

Первое ограничение касается достижимости, второе - ацикличности и третье - чтобы узел не имел более одного родителя.

Answer 2

Поскольку вы пропустили некоторые детали вашего кода, исходя из предположения, что все предикаты верны, данный код должен действительно описывать древовидную структуру в случаях Node, Обратите внимание, что это делается во всех случаях Node во вселенной, исключительно тем, isTreeТаким образом, никаких дополнительных предикатов не требуется.

Обратите внимание, что, хотя в вашем коде предполагается, что узлы (и дерево в целом) находятся в глобальной области видимости, может быть удобнее определить предикаты, которые определяют допустимое дерево в зависимости от заданных параметров, например, для acyclicity:

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, так как представление не позволяет этого, по построению.