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 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 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 innerNodes[r: node-> node]
Returns

All nodes that aren’t leaves

Return type

set Node

Predicates

pred undirected [r: node->node]

r is symmetric.

pred noSelfLoops[r: node->node]

r is irreflexive.

pred 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 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 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 ring [r: node->node]

r forms a single cycle.

pred dag [r: node->node]

r is a dag: there are no self-loops in the transitive closure.

pred forest [r: node->node]

r is a dag and every node has at most one parent.

pred tree [r: node->node]

r is a forest with a single root node.

pred treeRootedAt[r: node->node, root: node]

r is a tree with node root.