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: