import java.util.Vector;
import java.util.Enumeration;

class NodeNeighbors {
    // OVERVIEW: Record type for representing an edge.
    /*@non_null@*/ String node;
    /*@non_null@*/ StringSet neighbors; // A Set of String objects
    NodeNeighbors (/*@non_null@*/ String n) { node = n; neighbors = new StringSet (); }
}

public class Graph {
    // OVERVIEW: 
    //      A Graph is a mutable type that represents an undirected
    //      graph.  It consists of nodes that are named by Strings,
    //      and edges that connect a pair of nodes.
    //      A typical Graph is: < Nodes, Edges >
    //       where
    //         Nodes = { n1, n2, , nm }
    //       and 
    //         Edges = { {from_1, to_1}, ..., {from_n, to_n} }
    
    // Rep:
    Vector nodes; // Vector of NodeNeighbors objects

    // Rep Invariant:
    //
    // RI (c) = c.nodes != null
    //          && elements of c.nodes are NodeNeighbors objects
    //          && no duplicates in c.nodes
    //          && for each node in c.nodes, 
    //               each node in c.nodes[i].neighbors is a node in c.nodes
    //               c.nodes[i].neighbors does not contain duplicates
    //

    //@invariant nodes != null
    //@invariant nodes.containsNull == false
    //@invariant nodes.elementType == \type(NodeNeighbors)

    // Abstraction Function:
    //
    // AF (c) = < Nodes, Edges > where
    //    Nodes = { c.nodes[i].node | 0 <= i < c.nodes.size () } 
    //    Edges = { { c.nodes[i].node, c.nodes[i].neighbors[e] }
    //              | 0 <= i < c.nodes.size (),
    //                0 <= e <= c.nodes[i].neighbors.size ()
    //            } 

    // Creator 
    public Graph () { 
	// EFFECTS: Initializes this to a graph
	//      with no nodes or edges: < {}, {} >.

	nodes = new Vector ();
	//@set nodes.elementType = \type(NodeNeighbors);
	//@set nodes.containsNull = false;
    }
	
    private /*@non_null@*/ NodeNeighbors lookupNode (String name) {
	// REQUIRES: name is a node in this. 
	Enumeration nels = nodes.elements ();

	while (nels.hasMoreElements ()) {
	    NodeNeighbors current = (NodeNeighbors) nels.nextElement ();
	    if (current.node.equals (name)) {
		return current;
	    }
	}

	return null; 
    } //@nowarn NonNullResult // The requires clause was not satisfied!

    // Mutators

    public void addNode (String name) 
        //@requires name != null
	// REQUIRES: name is not the name of a node in this
	// MODIFIES: this
	// EFFECTS: adds a node named name to this:
	//     this_post = < this_pre.nodes U { name }, this_pre.edges >
    {
	nodes.addElement (new NodeNeighbors (name));
    }

    public void addEdge (String fnode, String tnode) 
	//@requires fnode != null ;
	//@requires tnode != null ;
    {
	// REQUIRES: fnode and tnode are names of nodes in this, there is no
	//    edge between fnode and tnode already in the graph.
	// MODIFIES: this
	// EFFECTS: Adds an edge from fnode to tnode to this:
	//       this_post = < this_pre.nodes, this_pre.edges U { {fnode, tnode} } >
	
	NodeNeighbors n1 = lookupNode (fnode);
	NodeNeighbors n2 = lookupNode (tnode);
	n1.neighbors.insert (tnode);
	n2.neighbors.insert (fnode);
    }

    // Observers
    public boolean hasNode (String node) {
	// EFFECTS: Returns true iff node is a node in this.
	Enumeration nels = nodes.elements ();
	while (nels.hasMoreElements ()) {
	    NodeNeighbors current = (NodeNeighbors) nels.nextElement ();
	    if (current.node.equals (node)) {
		return true;
	    }
	}
	
	return false;
    }

    public StringIterator nodes () {
	// EFFECTS: Returns the StringIterator that
	//      yields all nodes in this in arbitrary order.
	Vector nnames = new Vector ();
	//@set nnames.elementType = \type(String)
	//@set nnames.containsNull = false

	for (Enumeration e = nodes.elements (); e.hasMoreElements (); ) {
	    NodeNeighbors current = (NodeNeighbors) e.nextElement ();
	    nnames.addElement (current.node);
	}

	return (new StringIterator (nnames.elements ()));
    } //@nowarn Invariant // ESC/Java reports an invariant violation here, but we know we haven't changed the rep.

    public StringSet getNeighbors (String node) {
	// REQUIRES: node is a node in this
	// EFFECTS: Returns the StringSet consisting of all nodes in this
	//      that are directly connected to node:
	//         \result =  { n | {node, n} is in this.edges }

	NodeNeighbors n = lookupNode (node);
	return n.neighbors.copy ();
    }

    public String toString () {
	// EFFECTS: Returns a string representation of this.
	String res = "Graph:<Nodes: { ";
	boolean firstone = true;

	for (Enumeration e = nodes.elements (); e.hasMoreElements (); ) {
	    NodeNeighbors current = (NodeNeighbors) e.nextElement ();
	    if (firstone) {
		firstone = false;
	    } else {
		res += ", ";
	    }
	    res += current.node;
	}

	res += "}, Edges: { ";

	firstone = true;
	for (Enumeration e = nodes.elements (); e.hasMoreElements (); ) {
	    NodeNeighbors current = (NodeNeighbors) e.nextElement ();

	    for (Enumeration neighbors = current.neighbors.elements (); neighbors.hasMoreElements (); ) {
		//@set neighbors.returnsNull = false
		//@set neighbors.elementType = \type(String)
		String tnode = (String) neighbors.nextElement ();

		// should avoid printing every edge twice...
		if (tnode.compareTo (current.node) >= 0) {
		    if (firstone) {
			firstone = false;
		    } else {
			res += ", ";
		    }
		    
		    res += current.node + " <-> " + tnode;
		}
	    }
	}
	
	res += "}>";
	return res;
    }
}