Graphs.module
(*
These classes are the result of many discussions among David
Stoutamire, Jerry Feldman, Wolf Zimmerman and myself (Ben Gomes).
They borrow many ideas from Karla and LEDA. A couple of the
algorithms (bellman_ford and dijkstra) were translated from LEDA.
Constructing a graph:
g: DIGRAPH := #;
n1 ::= g.add_node; n2 ::= g.add_node; n3 ::= g.add_node;
g.connect(n1,n2).connect(n1,n3);
This constructs:
1
/\
2 3
Getting the nodes in depth first order:
l:LIST{INT} := #;
loop n: INT := DIGRAPH_ALG::dfs!(g);
l := l.append(n);
end;
Getting the layers of the graph:
l: LIST{SET{INT}} := #;
loop s: SET{INT} := DIGRAPH_ALG::layer!(g);
l := l.append(s);
end;
Graph Views
-----------
Views of the nodes of a graph:
g1: DIGRAPH{INT} := #;
g1n1 ::= g1.add_node(1); g1n2 ::= g.add_node(2); g1n4 ::= g.add_node(4);
Which constructs:
1
|
2 4
g2: DIGRAPH{INT} := #;
g2n1 ::= g1.add_node(1); g2n2 ::= g.add_node(2); g2n5 ::= g.add_node(5);
Which constructs:
1
|
2 5
We can now find the intesection of nodes in the two graphs by looking
at the edge view and then finding the intersection
node_view1:DIGRAPH_NODE_SET_VIEW{INT,DIGRAPH{INT}} := #(g1);
node_view2:DIGRAPH_NODE_SET_VIEW{INT,DIGRAPH{INT}} := #(g2);
Finding the union of the nodes in two graphs:
u: $RO_SET{INT} := node_view1.union(node_view2); = {1,2,4,5}
Finding the difference between the sets of nodes in two graphs:
u: $RO_SET{INT} := node_view1.diff(node_view2); = {4,5}
Views of the edges of a graph:
The following graph is used in several of the following examples
graph_n3_n4_n1: DIGRAPH{INT} := #;
n3 ::= g.add_node(3);
n4 ::= g.add_node(4);
n1 ::= g.add_node(1)
graph_n3_n4_n1 is n3->n4<-n1
es: DIGRAPH_EDGE_SET_VIEW{INT,DIGRAPH{INT}} := #(graph_n3_n4_n1);
Th set of edge, 'es' is {#DIEDGE{INT}(3,4) #DIEDGE{INT}(1,4) }
There are also views of the incoming and outgoing nodes of a particular
node in the graph i.e. views of neighbors of a node:
inc: DIGRAPH_INC_SET_VIEW{INT,DIGRAPH{INT}} := #(graph_n3_n4_n1,n4);
The set 'inc' consists of all the incoming nodes into the node 'n4',
which consists of the nodes {3,1}. This set may be used to determine
whether two different nodes have any common incoming edges
outg: DIGRAPH_OUTG_SET_VIEW{INT,DIGRAPH{INT}} := #(graph_n3_n4_n1,n3);
The set 'outg' consists of all the outgoing nodes from the node 'n3'
which consists of the element n4 i.e. 4
View of the nodes as a reversed graph:
rg ::= #DIGRAPH_REV_DIGRAPH_VIEW{INT}(graph_n3_n4_n1);
rg is then the graph 3 <- 4-> 1
Thus, we would have the following
#OUT+rg.has_edge(#DIEDGE{INT}(4,3)); -- Prints true
#OUT+rg.has_edge(#DIEDGE{INT}(3,4)); -- Prints false
A View of a graph filtered through a node predicate:
g ::= #DIGRAPH{INT};
n1 ::= g.add_node(1); n2 ::= g.add_node(2); n3 ::= g.add_node(3);
n4 ::= g.add_node(4); n5 ::= g.add_node(5); n0 ::= g.add_node(0);
g.connect(n3,0); g.connect(n1,n2); g.connect(n2,n4);
g.connect(n2,n5); g.connect(n1,n3);
1
/\
2 3
/ \ \
4 5 0
Now consider the following node filter routine, which only permits
nodes which are less than 4
node_rout:ROUT{INT}:BOOL := bind(_:INT.is_lt(4));
fv:FILTERGRAPH_DIGRAPH_VIEW{INT,DIGRAPH{INT}} := #(g,node_rout);
fv is now of the form
1
/\
2 3
\
0
A Few Algorithms on Weighted Graphs
-----------------------------------
Bellman Ford for shortest paths and predecessors in
the shortest path tree:
g: WTD_DIGRAPH{INT,FLT} := #;
-- A weighted graph with nodes of type
-- INT and node and edge weights of type FLT
n1: INT := g.add_node(1);
n2: INT := g.add_node(2);
n3: INT := g.add_node(3);
n4: INT := g.add_node(4);
g.connect(n1,n2,10.0); g.connect(n1,n3,11.0);
etc. until we have
*1*
10.0/ | \ 11.0
/ 1.0 \
*2* | *3*
13.0 \ | / 11.0
\ | /
*4*
distances: MAP{INT,FLT};
preds: MAP{INT,INT}; -- Predecessor mapping
res::=g.bellman_ford(n1,out distances, out preds);
Distances maps nodes (of type INT) to the FLT distance from the source
node (the node n1 is supplied is supplied as the source). Thus,
node[4] is at distance 1.0 via the edge (1,4) preds maps nodes to
their predecessor in the shortest path tree And the precedessor of
node[4] in the shortest path tree is 1. The full mappings returned
are:
distances[4] = 1.0 [3] = 11.0 [2] = 10.0
preds[4] = 1 [3] = 1 [2] = 1
Dijkstra algorithm for single source shortest paths if the
graph has non-negative weights. Very similar, but more
efficient than bellman ford, if the graph has no negative
weights
max_weight_path_node! Yields successive nodes along the maximum weight
path in the graph. Using the same graph as before:
res: A_LIST{INT} := #;
loop res.append(g.max_weight_path_node!(g,n1,n4)); end;
n1 is specified as the source node and n4 is specified as the sink
node. The result, which is stored as elements of the list "res" will
simply consist of n1,n2,n4, whose path has a weight of 23
*)
-- Abstract and concrete edges
edges.sa -has edges.sa
$EDGE
UEDGE
DIEDGE
-- Abstraction over all graphs, parametrized over node and edge types
abs_graph.sa -has abs_graph.sa
$GRAPH
-- Graph exceptions
graph_exc.sa -has graph_exc.sa
GRAPH_EXC
-- Abstract digraphs
abs_digraph.sa -has abs_digraph.sa
$RO_DIGRAPH
$DIGRAPH
-- Digraphs
digraph_incl.sa -has digraph_incl.sa
RO_DIGRAPH_INCL
DIGRAPH_INCL
-- Various views of a digraph
digraph_views.sa -has digraph_views.sa
DIGRAPH_NODE_SET_VIEW
DIGRAPH_EDGE_SET_VIEW
DIGRAPH_INC_SET_VIEW
DIGRAPH_OUTG_SET_VIEW
DIGRAPH_REV_DIGRAPH_VIEW
FILTERGRAPH_DIGRAPH_VIEW
digraph.sa -has digraph.sa
DIGRAPH
digraph_alg.sa -has digraph_alg.sa -- Directed graph algorithms
DIGRAPH_ALG
test_digraph.sa -has test_digraph.sa
TEST_DIGRAPH
test_digraph_views.sa -has test_digraph_views.sa
TEST_DIGRAPH_VIEWS
-- Undirected graphs
abs_ugraph.sa -has abs_ugraph.sa
$RO_UGRAPH
$UGRAPH
ugraph_incl.sa -has ugraph_incl.sa
UGRAPH_INCL
ugraph.sa -has ugraph.sa -- An undirected digraph implementation
UGRAPH
test_ugraph.sa -has test_ugraph.sa -- Undirected graph test
TEST_UGRAPH
-- labelled digraphs
lbld_digraph.sa -has lbld_digraph.sa
$LBLD_DIGRAPH
LBLD_DIGRAPH_INCL
LBLD_DIGRAPH
wtd_digraph.sa -has wtd_digraph.sa
WTD_DIGRAPH
wtd_digraph_alg.sa -has wtd_digraph_alg.sa
WTD_DIGRAPH_ALG
test_wtd_digraph.sa -has test_wtd_digraph.sa
TEST_WTD_DIGRAPH
-- Dumping to dot
--graph_to_dot.sa -has graph_to_dot.sa $SUPPORTS_DOT DIGRAPH_TO_DOT TEST_DIGRAPH_TO_DOT