CODEWITHSUNDEEP
closuresalloy
Asif Shiraz
Asif Shiraz

Reputation: 874

Reflexive Transitive Closure in Alloy in Ternary Operator

I have an alloy model

sig BinaryTree{
    root : Node,
    nodes: set Node,
    left, right : Node -> Node
}

Now, I have a predicate defined over it, which is valid syntax

pred Connected[t: BinaryTree, l:Node -> Node, r: Node -> Node]
{
    all n: t.nodes | n in t.root.*(l+r)
}

However, I do not understand why it is valid, because the behavior of *, the reflexive transitive closure says that for

foo.*bar

you get the set of everything you can possibly get by applying bar to foo repeatedly. Thus, foo, foo.bar, foo.bar.bar etc.

However, what you get, is always the result of "bar", not something different. The result of applying the closure, must always be of "Type" bar.

In the code example I gave above, the result should always be (l+r), which means a set contains types (node->node).

But the "in" keyword that I'm applying to n, should really apply to a set of (node), and not (node->node). Why does this work? Why is it implicitly transforming (node->node) to a set of (nodes), such that n: node is being evaluated against this set for inclusion in it?

Upvotes: 1

Views: 419

Answers (1)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

Your misunderstanding comes from the type you give to fields.

In your example the field root is not of type Node but of type BinaryTree -> Node as it relates a BinaryTree to a Node.

Just like your the field root, the relation Node -> Node is also of arity 2.

If you simply reason about types, the following can represent your predicate :

Node in BinaryTree . BinaryTree -> Node . *(Node -> Node + Node -> Node )

which when developped : 

Node in BinaryTree . BinaryTree -> Node . *(Node -> Node)

the * operator simply "reverse" a relation, so that A->B tuples become B->A tuples. You then have :

Node in BinaryTree . BinaryTree -> Node . (Node -> Node)

Now to illustrate how the "." (dot join) operator is used, consider the example : A1 . A2->B With A1, A2 and B being sets of atoms of signature A and B respectively, this expression returns the set of B-atoms present in a A2->B such that A2 is in A1.

The type left hand-side of the dot operator is thus removed to the type of the relation following.

We thus have finally :

Node in Node .(Node->Node) 

Node in Node

I hope you understand why it works now :)

Upvotes: 3

Related Questions