/** Get the weight of an edge  
   */
  protected int weight(Edge e) {
    return ((Integer) e.get(WEIGHT)).intValue();
  }
  /** Attribute for vertex distances 
   */
  protected Object DIST = new Object();
  /** Set the distance of a vertex. 
   */
  protected void setDist(Vertex v, int d) {
    v.put(DIST, new Integer(d));
  }
  /** Decoration key for entries in the priority queue 
   */
  protected Object ENTRY = new Object();
  /** Get the entry decoration of a vertex. 
   */
  protected Entry getEntry(Vertex v) {
    return (Entry) v.get(ENTRY);
  }
  /** Set the entry decoration of a vertex 
   */
  protected void setEntry(Vertex v, Entry e) {
    v.put(ENTRY, e);
  }
  /** Remove the entry decoration of a vertex 
   */
  protected void removeEntry(Vertex v) {
    v.remove(ENTRY);
  }
  /** Get the vertex associated with an entry 
  */
  protected Vertex getVertex(Entry e) {
    return (Vertex) e.value();
  }
  /** Get the distance of a vertex given its entry 
   */
  protected int getDist(Entry e) {
    return ((Integer) e.key()).intValue();
  }
} // end of Dijkstra class