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
usesrootedAt
and notroots
.

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
. Ifr
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
noSelfLoops[r: node>node]
¶ r
isirreflexive
.

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
usesrootedAt
and notroots
.

pred
ring [r: node>node]
¶ r
forms a single cycle.

pred
dag [r: node>node]
¶ r
is a dag: there are no selfloops 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 noderoot
.