Graph Utilities For Subsets

Filed under:

alloy modeling utilities

The graph utilities that ship with Alloy are extremely useful for setting up topologies. However, a few of the predicates enforce properties to hold true over the entire supplied signature. In most cases this is the desired behavior, but occasionally it is useful to enforce the properties over a subset of the signature’s atoms.

For example, the stronglyConnected predicate is defined as follows:

module util/graph[node]

pred stronglyConnected [r: node->node] {
    all n1, n2: node | n1 in n2.*r
}

Note that the constraint here is all n1, n2: node, meaning that every atom in the node signature is used to enforce the predicate. Now suppose you have some relation that is of the form node->node, but only some subset of the atoms in the node signature is in this relation. If you still want to enforce that this relation be strongly connected, the previous predicate will not do so. However, you can instead use the following predicate:

module graphSubsets[node]

pred stronglyConnectedSubset [r: node->node] {
    let a = dom[r] + ran[r] | all n1, n2: a | n1 in n2.*r
}

The relation r must still be of the form node->node, but only those atoms that appear within the relation are used to enforce that the relation is strongly connected. The following Alloy module contains a number of the graph predicates translated in to this form:

graphSubsets.als

Finally, if you are looking to enforce that some generic relation is strongly connected with complete disregard for the type of atoms within the relation, the following may be used:

pred stronglyConnectedGeneric [r: univ->univ] {
    let a = dom[r] + ran[r] | all n1, n2: a | n1 in n2.*r
}