graph

Graph provides predicates on relations over a parameterized signature.

open util/graph[Node]

sig Node {
  edge: set Node
}

run {
  dag[edge]
}

Notice that graph is parameterized on the signature, but the predicate takes in a relation. This is so that you can apply multiple predicates to multiple different relations, or different subsets of the same relation. The graph module uses some specific terminology:

This means that in a completely unconnected graph, every node is both a root and a leaf.

Functions

fun graph.roots[r: node-> node]

Return type:: set Node

Returns the set of nodes that are not connected to by any other node.

Warning

this is not the same meaning of root as in the rootedAt predicate! For the predicate, a root is a node that transitively covers the whole graph. Internally, util/graph uses rootedAt and not roots.

fun graph.leaves[r: node-> node]

Return type:: set Node

Returns the set of nodes that do not connect to any other node.

Note

If r is empty, roots[r] = leaves[r] = Node. If r is undirected or contains enough self loops, roots[r] = leaves[r] = none.

fun graph.innerNodes[r: node-> node]

Returns:: All nodes that aren’t leaves
Return type:: set Node

Predicates

pred graph.undirected [r: node->node]: r is symmetric.

pred graph.noSelfLoops[r: node->node]: r is irreflexive.

pred graph.weaklyConnected[r: node->node]: For any two nodes A and B, there is a path from A to B or a path from B to A. The path may not necessarily be bidirectional.

pred graph.stronglyConnected[r: node->node]: For any two nodes A and B, there is a path from A to B and a path from B to A.

pred graph.rootedAt[r: node->node, root: node]: All nodes are reachable from root.

Warning

this is not the same meaning of root as in the roots function! For the function, a root is a node no node connects to. Interally, util/graph uses rootedAt and not roots.

pred graph.ring [r: node->node]: r forms a single cycle.

pred graph.dag [r: node->node]: r is a dag: there are no self-loops in the transitive closure.

pred graph.forest [r: node->node]: r is a dag and every node has at most one parent.

pred graph.tree [r: node->node]: r is a forest with a single root node.

pred graph.treeRootedAt[r: node->node, root: node]: r is a tree with node root.