### 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.

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

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: 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.

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: 