// This program demonstrates an algorithm designed from its key loop
// invariants. The algorithm finds the shortest route from a starting point
// to all other points on a map (technically, it is Dijkstra's algorithm for
// finding shortest paths in a graph).
// History:
//
// February 2007 -- Created by Doug Baldwin as a prototype solution to a
// CSci 240 exercise.
public class LoopInvariants {
// The algorithm for finding the shortest distances from a starting point
// to all other points in a map. The map consists of points (e.g., street
// intersections) and the distances between those points that are directly
// connected (e.g., intersections with a segment of street between them).
// This information is represented by a 2-dimensional array, A, of numbers,
// where A[i][j] is the distance from point i to point j. If there is no
// direct connection between points i and j, A[i][j] should be the constant
// INFINITY. Note that this representation of maps assumes that points in the
// map are identified by the integers 0, 1, 2, etc. It also implies that A is
// square. The other parameter to this method is such an integer, indicating
// the point at which the shortest distance computation is to start. The
// method returns an array of distances from that starting point to all
// points in the map.
//
// This algorithm classifies map points (aka "nodes") into 2 sets: those
// nodes to which the shortest distance from the start node is known, and
// those to which only a bound (possibly infinite) is known. The former nodes
// are said to be "finalized," and their distances are said to be "final."
// Distances to both kinds of nodes (minimal distances for finalized nodes, and
// bounds on minimal distance for unfinalized ones) are recorded in a "distances"
// array. The algorithm reduces the set of unfinalized nodes one by one,
// maintaining the loop invariant that the entry in the distances array for
// unfinalized node i is the minimal distance from the start node to node i *if
// one visits only finalized nodes* between the start node and i (exclusive
// of the start node and i).
public static final double INFINITY = 1.0e100;
static double[] findDistances( double[][] map, int start ) {
final int n = map.length; // The number of nodes in the system
double[] distances = new double[ n ];
boolean[] finalized = new boolean[ n ]; // finalized[i] = true iff distances[i] is final
// Initialize the distances and finalized arrays. Initially no nodes are finalized,
// and all distances are bounded by infinity, except for the distance from the start
// node to itself, which is 0.
for ( int i = 0; i < n; i++ ) {
distances[i] = INFINITY;
finalized[i] = false;
}
distances[start] = 0.0;
// Now shrink the bounds in the distances array until all become final. To do this,
// note that the loop invariant implies that at the start of each iteration of the
// loop, the smallest supposedly unfinalized distance is actually final. This is
// because any distance from the start node to the node with that smallest distance
// (node m) would have to be from the start node via some (possibly 0) finalized nodes,
// and then via at least one unfinalized one (otherwise the distance is along a path
// that only goes via finalized nodes, and so is the distance already recorded in the
// distances array, by the loop invariant). But getting from the start node to the first
// unfinalized node on this hypothetical path involves a distance greater than the
// distance from the start node to node m using only finalized nodes. Given this fact,
// the node with the minimal distance can be moved to finalized node set. Then, in order
// to maintain the loop invariant, distances to other unfinalized nodes have to be checked
// and possibly updated, since the new finalized node may provide a shorter route to them
// than was possible without that node. Since each iteration of this loop reduces the
// number of unfinalized nodes by 1, and initially all nodes were unfinalized, the loop
// has to repeat n times.
for ( int i = 0; i < n; i++ ) {
// Find the first unfinalized node. This loop has the invariant that at the start of
// each iteration, nodes 0 through j-1 are known to be finalized.
int j = 0;
while ( j < n && finalized[j] ) {
j = j + 1;
}
// Find the unfinalized node with minimal distance from the start. This loop is based
// on the invariant that m is the index of the unfinalized node with the
// the least distance in nodes 0 through j-1 at the start of each iteration of the loop.
int m = j;
j = j + 1;
while ( j < n ) {
if ( ! finalized[j] && distances[j] < distances[m] ) {
m = j;
}
j = j + 1;
}
// Make the minimal-distance unfinalized node (node m) final.
finalized[m] = true;
// Update distance bounds for the remaining unfinalized nodes. This loop is based on
// the invariant that at the beginning of each iteration, nodes 0 through k-1 have
// distances conforming to the main loop invariant, given the new final node m.
for ( int k = 0; k < n; k++ ) {
if ( distances[m] + map[m][k] < distances[k] ) {
distances[k] = distances[m] + map[m][k];
}
}
}
// There are no unfinalized nodes left, so the distances array must contain only
// final (i.e., shortest) distances. Return it.
return distances;
}
// The main method simply demonstrates the others.
public static void main (String args[]) {
// Demonstrate shortest paths in a map.
// An artificial "map" in which intersections form a single "street," with
// intersections 1 unit apart:
double[][] testMap = { { 0.0, 1.0, INFINITY, INFINITY, INFINITY },
{ 1.0, 0.0, 1.0, INFINITY, INFINITY },
{ INFINITY, 1.0, 0.0, 1.0, INFINITY },
{ INFINITY, INFINITY, 1.0, 0.0, 1.0 },
{ INFINITY, INFINITY, INFINITY, 1.0, 0.0 } };
// A map of part of the north edge of the Geneseo campus, based on MapQuest with
// distances in feet, estimated by eyeball. Intersections are...
// 0: The corner of Main St. and University Dr.
// 1: The intersection of University Dr. and Wadsworth St.
// 2: The intersection of University Dr. and Franklin St.
// 3: The intersection of University Dr. and Court St.
// 4: The intersection of Court St. and Franklin St.
// 5: The intersection of Court St. and Wadsworth St.
// 6: The intersection of Court St. and Main St.
double[][] geneseoMap = { { 0.0, 450.0, INFINITY, INFINITY, INFINITY, INFINITY, 600.0 },
{ 450.0, 0.0, 400.0, INFINITY, INFINITY, 800.0, INFINITY },
{ INFINITY, 400.0, 0.0, 800.0, 700.0, INFINITY, INFINITY },
{ INFINITY, INFINITY, 800.0, 0.0, 200.0, INFINITY, INFINITY },
{ INFINITY, INFINITY, 700.0, 200.0, 0.0, 300.0, INFINITY },
{ INFINITY, 800.0, INFINITY, INFINITY, 300.0, 0.0, 500.0 },
{ 600.0, INFINITY, INFINITY, INFINITY, INFINITY, 500.0, 0.0 } };
double[] distances = findDistances( geneseoMap, 0 );
System.out.println( "Distances from point 0:" );
for ( int i = 0; i < distances.length; i++ ) {
System.out.println( "\tto point " + i + ": " + distances[i] );
}
}
}