CODEWITHSUNDEEP
treerelationalalloycalculus
Ellie A.
Ellie A.

Reputation: 11

Alloy: checking a tree relationship with a predicate

Was wondering how to describe a tree relationship in the form of:

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

if I have:

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
}

I was wondering how the above constraints on a tree can be modeled with r: univ -> univ.

Thank you so much in advance!

Upvotes: 1

Views: 454

Answers (2)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

I see that you are interested in checking if a relation satisfies the constraints of a tree in a generic way, that is, independently of the type of the relation.

This is possible in Alloy, the trick being that for any relation r: univ->univ, r.univ will give you the domain of the relation and univ.r will give you the range of the relation (from it you can get all the nodes concerned by the relation).

The predicate you are looking for is thus : 

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

The first constraint is for reachability, second for acyclicness and third to prevent a node from having more than one parent.

Upvotes: 3

ivcha
ivcha

Reputation: 463

Since you've omitted some of the details of your code, under the assumption that all of the predicates are correct, the given code should indeed describe a tree structure on the instances of Node. Note that this is done on all the instances of Node in the universe, solely by the fact isTree, thus no additional predicate is required.

Note that while your code assumes nodes (and the tree overall) is in the global scope, it might be more convenient to define predicates that define a valid tree depending on the given parameters, like e.g. for acyclicity:

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

In this case, the tree is defined with a root note and a relation that defines parent-child relation. Afterwards, to define (constrain a model to) a valid tree, one might write something along the lines of

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

Note in such case, you might not need to model constraint noDoubleEdges, since the representation does not allow it, by construction.

Upvotes: 1

Related Questions