/** The actual execution of Dijkstra's algorithm.
    * @param v source vertex.  
    */
  protected void dijkstraVisit (Vertex v) {
    // store all the vertices in priority queue Q
    for (Iterator vertices = graph.vertices(); vertices.hasNext();) {
      Vertex u = (Vertex) vertices.next();
      int u_dist;
      if (u==v)
	u_dist = 0;
      else
	u_dist = INFINITE;

      Entry u_entry = Q.insert(new Integer(u_dist), u);
      setEntry(u, u_entry);
    }
    // grow the cloud, one vertex at a time
    while (!Q.isEmpty()) {
      // remove from Q and insert into cloud a vertex with minimum distance
      Entry u_entry = Q.min();
      Vertex u = getVertex(u_entry);
      int u_dist = getDist(u_entry);
      Q.remove(u_entry); // remove u from the priority queue
      setDist(u, u_dist); // the distance of u is final
      removeEntry(u); // remove the entry decoration of u
      if (u_dist == INFINITE)
	continue; // unreachable vertices are not processed
      // examine all the neighbors of u and update their distances
      for (Iterator edges = graph.incidentEdges(u); edges.hasNext();) {
	Edge e = (Edge) edges.next();
	Vertex z = graph.opposite(u,e);
	Entry z_entry = getEntry(z);
	if (z_entry != null) { // check that z is in Q, i.e., not in the cloud
	  int e_weight = weight(e);
	  int z_dist = getDist(z_entry);
	  if ( u_dist + e_weight < z_dist ) // relaxation of edge e = (u,z)
	    Q.replaceKey(z_entry, new Integer(u_dist + e_weight));
	}
      }
    }
  }