Extracting Subsets Of Relations

Filed under:

alloy modeling utilities

In Graph Utilities for Subsets we discuss how to use some of the predicates that ship with the graph utilities in Alloy on a subset of atoms in a relation as opposed to the default behavior, which is to require every atom in the supplied signature to be present in the relation. Here we’ll look at how to use the restriction operators to create subsets of relations that can be used with these utilities.

Let’s begin with a very simple Alloy model of a graph.

abstract sig Node {
    link: set Node
}

lone sig A, B, C, D, E extends Node {}

pred show {}
run show for exactly 5 Node

Here we’ve created a graph containing exactly 5 nodes and no restrictions on how those nodes are connected. Running show generates the following instance:

A simple, unrestricted graph

Now let’s say we want to enforce some properties on a subset of the graph. The following functions can be used to extract various subsets of the link relation:

-- Include only links that originate from a node found in nodeset
fun linksBeginningWith (nodeset: set Node): set Node->Node {
    nodeset <: link
}

-- Include only links that end at a node found in nodeset
fun linksEndingWith (nodeset: set Node): set Node->Node {
    link :> nodeset
}

-- Include only links that begin and end at nodes found in nodeset
fun linksThatIncludeOnly (nodeset: set Node): set Node->Node {
    nodeset <: link :> nodeset
}

Note that each of these functions simply uses the <: and :> operators. These operators are called the domain and range restriction operators, respectively. The way they operate is very simple. If you imagine a binary relation, like the link relation above, as a table with two columns, the “domain” of the relation would be the left column and the “range” of the relation would be the right column. In fact, more recent versions of Alloy will print a table view of relations by default. If you open the evaluator while looking at the instance above and ask it to print the link relation, you’ll see the following:

Table showing the link relation

The domain and range restriction operators simply filter a relation to a given domain or range, i.e., they give us only the tuples whose domain or range include atoms in the provided set. The linksBeginningWith function simply gives us only those tuples found in the link relation that start with an atom found in nodeset. Similarly, the linksEndingWith function gives us the tuples that end with an atom found in nodeset. And finally, the linksThatIncludeOnly function applies both the domain and range restriction operators, giving us only the tuples that are entirely composed of atoms found in nodeset.

Going back to our example, let’s say we want to enforce some properties on only a subset of the graph – we want the subset of the graph consisting of nodes A, B, and C to be strongly connected, undirected, complete, and to not include any self loops.

open graphSubsets[Node] -- stronglyConnectedSubset
open util/graph[Node]   -- undirected, noSelfLoops
open util/relation      -- complete

abstract sig Node {
    link: set Node
}

lone sig A, B, C, D, E extends Node {}

---

fun linksThatIncludeOnly (nodeset: set Node): set Node->Node {
    nodeset <: link :> nodeset
}

---

pred show {
    let nodes = A+B+C, links = linksThatIncludeOnly[nodes] |
        stronglyConnectedSubset[links] and
        undirected[links] and
        complete[links, nodes] and
        noSelfLoops[links]
}

run show for exactly 5 Node

If we run this model and step through each instance, we can see that all of those properties will always hold for the subset of the graph that contains nodes A, B, and C, while the rest of the graph remains unrestricted, as shown in the following instance:

A subset of the graph has certain properties enforced