/** The actual execution of Dijkstra's algorithm.
    * @param v source vertex.  */
  protected void dijkstraVisit (Vertex v) {
    // initialize the priority queue Q and store all the vertices in it
    Q = new ArrayHeap(new IntegerComparator());
    for (VertexIterator vertices = graph.vertices(); vertices.hasNext();) {
      Vertex u = vertices.nextVertex();
      int u_dist;
      if (u==v)
	u_dist = 0;
      else
	u_dist = INFINITE;
      // setDist(u, u_dist);
      Locator u_loc = Q.insert(new Integer(u_dist), u);
      setLoc(u, u_loc);
    }
    // grow the cloud, one vertex at a time
    while (!Q.isEmpty()) {
      // remove from Q and insert into cloud a vertex with minimum distance
      Locator u_loc = Q.min();
      Vertex u = getVertex(u_loc);
      int u_dist = getDist(u_loc);
      Q.remove(u_loc); // remove u from the priority queue
      setDist(u, u_dist); // the distance of u is final
      destroyLoc(u); // remove the locator associated with u
      if (u_dist == INFINITE)
	continue; // unreachable vertices are not processed
      // examine all the neighbors of u and update their distances
      for (EdgeIterator edges = graph.incidentEdges(u); edges.hasNext();) {
	Edge e = edges.nextEdge();
	Vertex z = graph.opposite(u,e);
	if (hasLoc(z)) { // check that z is in Q, i.e., it is not in the cloud
	  int e_weight = weight(e);
	  Locator z_loc = getLoc(z);
	  int z_dist = getDist(z_loc);
	  if ( u_dist + e_weight < z_dist ) // relaxation of edge e = (u,z)
	    Q.replaceKey(z_loc, new Integer(u_dist + e_weight));
	}
      }
    }
  }