package edu.neu.ccs.demeter.aplib;

import java.util.*;

/** A traversal graph TG(S,G,N,B) is constructed from an encapsulated
    strategy S, a class graph G, a name map N for S and G, and a
    constraint map B for S and G according to a modified version of
    Algorithm 1 in the paper
    <a href="http://www.ccs.neu.edu/research/demeter/biblio/strategies.html">"Traversals
    of Object Structures: Specification and Efficient Implementation"</a>
    (the modifications allow G to be non-simple and N
    to be a relation instead of a function).  TG is essentially a
    compilation (that is, a compact and efficient generator) of the
    set of paths through G that is selected by S.  Conceptually,
    TG(S,G,N,B) consists of a graph G'' and a set T<sub>s</sub> of
    start nodes in G'', where G'' is (a subset of) n copies of G,
    where n is the number of edges in S, with some extra edges to
    connect nodes in different copies.  However, to keep the
    representation more compact, G'' is represented as two sets, NS
    and ES:
    <ul>
      <li>NS is a set of pairs (v, IS) where v is a node in G and IS is a
        set of indices i such that v<sup>i</sup> is in G''.
      <li>ES is a set of pairs (u <code>-l-&gt;</code> v, IM)
        where u <code>-l-&gt;</code> v is an edge
        in G and IM is a set of pairs of indices (i,j) such that
	u<sup>i</sup> <code>-l-&gt;</code> v<sup>j</sup> is in G''.
    </ul>
*/
public class TraversalGraph extends Traversal {
  /**
   * Compute the traversal graph TG(S,G,I,B<sub>TRUE</sub>) and start
   * and finish sets T<sub>s</sub> and T<sub>f</sub>, where I is the
   * identity map and B<sub>TRUE</sub> returns true for all graph
   * elements.
   *
   * @throws TraversalException if the resulting traversal
   * graph is empty.
   */	
  public TraversalGraph(SimpleStrategyI S, ClassGraphI G)
    throws TraversalException
  {
    this(S,G,null,null);
  }

  /**
   * Compute the traversal graph TG(S,G,N,B) and start and finish sets
   * T<sub>s</sub> and T<sub>f</sub>.  If N is null, the default name
   * map is used (the identity map).  If B is null, the default
   * constraint map is used (B<sub>TRUE</sub>, which returns true for
   * all graph elements).  B is conjoined with the constraint map B'
   * specified by the encapsulated strategy S; that is, an element e
   * of G is allowed in TG iff both B(i)(e) and B'(i)(e) are true.
   *
   * @throws TraversalException if:
   * <ul>
   *   <li>N maps symbolic node names in S to nodes that don't exist in G; or
   *   <li>TG(S,G,N,B) is empty.
   * </ul>
   */	
  public TraversalGraph(SimpleStrategyI S, ClassGraphI G,
			NameMapI N, final ConstraintMapI B)
    throws TraversalException
  {
    super(G);
    strategy = S;
    nameMap = N;
    
    if (nameMap == null)
      nameMap = new NameMapI() {
	  // Identity name map.  Map l to CG node labeled l.
	  public Collection get(String l, ClassGraphI CG)
	    throws NoSuchClassGraphNodeException
	  { return Collections.singleton(CG.getNode(l)); }
	  public boolean match(String l, Object cgv)
	  { return l.equals(String.valueOf(cgv)); }
	  public boolean match(String l, String cgl)
	  { return l.equals(cgl); }
	  public String toString()
	  { return "I"; }
	};

    final ConstraintMapI Bprime = strategy.getConstraintMap();
    if (Bprime == null)
      constraintMap = B;
    else if (B == null)
      constraintMap = Bprime;
    else
      constraintMap = new ConstraintMapI() {
	  // Combine B with B'.
	  public boolean meetsConstraint(int i, Object v, NameMapI NM) {
	    return B.meetsConstraint(i, v, NM) &&
	      Bprime.meetsConstraint(i, v, NM);
	  }
	  public boolean meetsConstraint(int i, EdgeI e, NameMapI NM) {
	    return B.meetsConstraint(i, e, NM) &&
	      Bprime.meetsConstraint(i, e, NM);
	  }
	  public boolean meetsConstraint(Object a, Object v, NameMapI NM) {
	    return B.meetsConstraint(a, v, NM) &&
	      Bprime.meetsConstraint(a, v, NM);
	  }
	  public boolean meetsConstraint(Object a, EdgeI e, NameMapI NM) {
	    return B.meetsConstraint(a, e, NM) &&
	      Bprime.meetsConstraint(a, e, NM);
	  }
	};

    strategyGraph = strategy.getStrategyGraph();
    copies = strategyGraph.numEdges();

    addSourceAndTargetEdges();
    markForward();
    markBackward();
    makeStartSet();
    makeFinishSet();

    // Check to see if at least one source node and at least one
    // target node were marked.
    // FIXME: is this the right error condition?
    // maybe check all sources and targets were marked?
    if (getStartSet().isEmpty() || getFinishSet().isEmpty())
      throw new TraversalException("No paths found matching strategy "
				   + strategy);
  }

  SimpleStrategyI strategy;
  NameMapI nameMap;
  ConstraintMapI constraintMap;

  /** The strategy S used in computing this traversal graph. */
  public SimpleStrategyI getStrategy() { return strategy; }

  /** The name map N for S and G used in computing this traversal graph. */
  public NameMapI getNameMap() { return nameMap; }

  /** The constraint map B for S and G used in computing this
      traversal graph. */
  public ConstraintMapI getConstraintMap() { return constraintMap; }

  /** The strategy graph of S. */
  StrategyGraphI strategyGraph;

  /** The number of edges in S, as well as the number of copies of G
      in the traversal graph.  Known as k in
      <a href="http://www.ccs.neu.edu/research/demeter/biblio/strategies.html">the paper</a>. */
  int copies;

  /** Set this for debugging output. */
  public static boolean debug = false;

  /** Maps from class graph nodes to NodeSet objects representing the
      set of indices for that node that are targets of source edges
      or sources of target edges, respectively. */
  LinkedHashMap
    sourceNodeSets = new LinkedHashMap(),
    targetNodeSets = new LinkedHashMap();

  /** Compute the set of source edges s<sup>*</sup> -&gt; v<sup>i</sup>
      and target edges v<sup>i</sup> -&gt; t<sup>*</sup>. */
  void addSourceAndTargetEdges() throws TraversalException {        
    // We don't actually add s* and t* and edges, just mark the nodes
    // that are connected to the endpoints.
    markEndpointNodes(sourceNodeSets, true);
    markEndpointNodes(targetNodeSets, false);
  }

  /** Mark the nodes connected to an endpoint (s* if source is true or t*
      if false) by adding them to the nodeSets. */
  void markEndpointNodes(Map nodeSets, boolean source)
    throws TraversalException
  {
    // For each strategy graph node a in s or t, for each class graph node
    // v in N(a), add the copies of v corresponding to the indices of the
    // incident edges of s or t.
    Collection sgNodeList =
      (source ? strategy.getSources() : strategy.getTargets());
    Iterator sgNodes = sgNodeList.iterator();
    while (sgNodes.hasNext()) {
      Object a = sgNodes.next();
      Collection indices = (source
			    ? strategyGraph.getOutgoingEdges(a)
			    : strategyGraph.getIncomingEdges(a));
      Collection cgNodeList = mapNode(a);
      // FIXME: can we avoid this step sometimes?
      if (cgNodeList == null) cgNodeList = classGraph.getNodes();
      Iterator cgNodes = cgNodeList.iterator();
      while (cgNodes.hasNext()) {
	Object v = cgNodes.next();
	NodeSet endpoints = (NodeSet) nodeSets.get(v);
	boolean newNodeSet = false;
	if (endpoints == null) {
	  endpoints = new NodeSet(v);
	  newNodeSet = true;
	}
	Iterator it = indices.iterator();
	boolean addedIndices = false;
	while (it.hasNext()) {
	  int i = ((Integer) it.next()).intValue();
	  endpoints.addIndex(i);
	  addedIndices = true;
	  if (source) markEndpointNodes_helper(i, v, endpoints);
	}
	if (newNodeSet && addedIndices) nodeSets.put(v, endpoints);
      }
    }
    if (debug) System.err.println((source ? "Source" : "Target")
				  + " nodes: " + nodeSets.values());
  }

  // Recursively check for other strategy graph nodes that match v and add
  // their outgoing edges to endpoints also.
  private void markEndpointNodes_helper(int i, Object v, NodeSet endpoints) {
    Object a = strategyGraph.getEdgeTarget(i);
    if (constraintMap.meetsConstraint(a, v, nameMap)) {
      Iterator it = strategyGraph.getOutgoingEdges(a).iterator();
      while (it.hasNext()) {
	int j = ((Integer) it.next()).intValue();
	if (!endpoints.hasIndex(j)) {
	  endpoints.addIndex(j);
	  markEndpointNodes_helper(j, v, endpoints);
	}
      }
    }
  }

  /** A set of class graph nodes corresponding to strategy graph node v
      using N and the encapsulated strategy name map.
      @returns null if v maps to all nodes.
      @throws TraversalException if the maps
      lead to a node that doesn't exist in G. */
  Collection mapNode(Object v) throws TraversalException {
    if (debug) System.err.print("TraversalGraph.mapNode(" + v + ")");
    Collection names = strategy.getNames(v);
    if (names == null) {
      if (debug) System.err.println(" = *");
      return null;
    }
    Collection nodes = new HashSet();
    Iterator namesIter = names.iterator();
    while (namesIter.hasNext()) {
      Collection vImage;
      try {
	vImage = nameMap.get((String) namesIter.next(), classGraph);
      } catch (NoSuchClassGraphNodeException e) {
	throw new TraversalException(e.getMessage());
      }
      if (vImage == null) return null;
      nodes.addAll(vImage);
    }
    if (debug) System.err.println(" = " + nodes);
    return nodes;
  }

  /** A map from EdgeI objects to Lists of IndexPair objects
      representing the intercopy endpoint indices for that edge. */
  Map icis = new HashMap();

  /** A List of IndexPair objects representing the endpoint indices of
      the intercopy copies of class graph edge e.
      If e = u <code>-l-&gt;</code> v,
      then u<sup>i</sup> <code>-l-&gt;</code> v<sup>j</sup>
      is in the traversal graph iff i == j or (i,j)
      is in getIntercopyIndices(e). */
  List getIntercopyIndices(EdgeI e) {
    List ici = (List) icis.get(e);
    if (ici == null) {
      icis.put(e, ici = new ArrayList());
      Iterator sgNodes = strategyGraph.getNodes().iterator();
      while (sgNodes.hasNext()) {
	Object a = sgNodes.next();
	Collection I = strategyGraph.getIncomingEdges(a);
	Collection O = strategyGraph.getOutgoingEdges(a);
	List cp = crossProduct(I, O);
	if (cp.isEmpty()) continue;
	if (constraintMap.meetsConstraint(a, e, nameMap) ||
	    constraintMap.meetsConstraint(a, e.getTarget(), nameMap)) {
	  if (debug) System.err.println("Adding intercopy edges for "
					+ edgeKey(e) + ": " + cp);
	  ici.addAll(cp);
	}
      }
      // Compute the transitive closure of the intercopy indices.
      // FIXME: this is probably incomplete, and/or slow...
      List add = new ArrayList();
      Iterator it1 = ici.iterator();
      while (it1.hasNext()) {
	IndexPair ip1 = (IndexPair) it1.next();
	Iterator it2 = ici.iterator();
	while (it2.hasNext()) {
	  IndexPair ip2 = (IndexPair) it2.next();
	  IndexPair ip3 = null;
	  if (ip1.getTarget() == ip2.getSource())
	    ip3 = new IndexPair(ip1.getSource(), ip2.getTarget());
	  else if (ip2.getTarget() == ip1.getTarget())
	    ip3 = new IndexPair(ip2.getSource(), ip1.getTarget());
	  if (ip3 != null && !add.contains(ip3) && !ici.contains(ip3))
	    add.add(ip3);
	}
      }
      if (debug) 
	System.err.println("Adding transitive closure intercopy edges for "
			   + edgeKey(e) + ": " + add);
      ici.addAll(add);
    }
    return ici;
  }


  /** The cross product, as a List of IndexPair objects, of Collections
      l1 and l2 of Integers.  E.g.
      <code>crossProduct({1, 2}, {3, 4}) = {<1,3>, <1,4>, <2,3>, <2,4>}</code>
  */
  List crossProduct(Collection l1, Collection l2) {
    if (debug) System.err.println(l1 + " x " + l2);
    List prod = new ArrayList();
    if (l1.isEmpty() || l2.isEmpty()) return prod;
    Iterator i1 = l1.iterator();
    while (i1.hasNext()) {
      int i = ((Integer) i1.next()).intValue();
      Iterator i2 = l2.iterator();
      while (i2.hasNext()) {
	int j = ((Integer) i2.next()).intValue();
	prod.add(new IndexPair(i, j));
      }
    }
    return prod;
  }

  /** Mark all nodes and edges in G'' reachable from s<sup>*</sup>. */
  void markForward() throws TraversalException {
    Iterator it = sourceNodeSets.values().iterator();
    while (it.hasNext()) markReachableFrom((NodeSet) it.next(), true);
  }

  /** Mark all nodes and edges in G'' from which t<sup>*</sup> is reachable. */
  void markBackward() throws TraversalException {
    Iterator it = targetNodeSets.values().iterator();
    while (it.hasNext()) markReachableFrom((NodeSet) it.next(), false);
  }

  /** Mark all nodes and edges in G reachable from the given nodes,
      following S, N, and B.  If forward is true, use forward links,
      otherwise use backward links. */
  void markReachableFrom(NodeSet nodes, boolean forward) {
    if (debug)
      System.err.println("markReachableFrom(" + nodes + ", " + forward + ")");
    for (int i = 0; i < copies; i++)
      if (nodes.hasIndex(i)) markReachable(nodes.getNode(), i, forward, null);
  }

  /** Mark all nodes and edges in G reachable from node v<sup>i</sup> following
      S, N, and B.  If forward is true, use forward links, otherwise
      use backward links.  The previous edge visited is prev (for
      checking knowledge path contraints). */
  void markReachable(Object v, int i, boolean forward, EdgeI prev) {
    if (debug) System.err.println("markReachable(" + v + ", " + i + ", "
				  + forward + ", " + edgeKey(prev) + ")");
    Collection edges;
    try {
      edges = (forward ?
	       classGraph.getOutgoingEdges(v) :
	       classGraph.getIncomingEdges(v));
    } catch (NoSuchClassGraphNodeException e) {
      // v is not in G, e.g. terminal class.
      // FIXME: disallow this?
      return;
    }
    if (!constraintMap.meetsConstraint(i, v, nameMap)) return;
    // Don't check marked(v,i,forward), because we might have been
    // here before by a different path that caused some outgoing edges
    // to be illegal (due to knowledge path restrictions), but might
    // be legal now.  This means we might visit a node multiple times,
    // but never more than the number of incoming edges.

    // We still need to mark the node, though, to make sure it gets
    // added to the final TG.
    mark(v, i, forward);
    Iterator it = edges.iterator();
    while (it.hasNext()) {
      EdgeI edge = (EdgeI) it.next();
      markReachableThroughEdge(edge, i, i, forward, prev);
      Iterator ici = getIntercopyIndices(edge).iterator();
      while (ici.hasNext()) {
	IndexPair ip = (IndexPair) ici.next();
	if (i == (forward ? ip.getSource() : ip.getTarget()))
	  markReachableThroughEdge(edge, ip.getSource(), ip.getTarget(),
				   forward, prev);
      }
    }
  }

  /** Mark all nodes and edges in G reachable through
      edge = v<sup>i</sup> -> u<sup>j</sup> following S, N, and B.
      If forward is true, use forward links, otherwise use backward links.
      The previous edge visited is prev (for checking knowledge path
      contraints). */
  void markReachableThroughEdge(EdgeI edge, int i, int j,
				boolean forward, EdgeI prev)
  {
    if (debug) System.err.println("markReachableThroughEdge(" + edgeKey(edge)
				  + ", " + i + ", " + j + ", " + forward + ", "
				  + edgeKey(prev) + ")");
    if (prev != null)
      if (forward
	  ? edge.isAlternationEdge() && prev.isInheritanceEdge()
	  : edge.isInheritanceEdge() && prev.isAlternationEdge()) {
	// Violates knowledge-path constraint.
	return;
      }
    if (!marked(edge, i, j, forward)
	&& constraintMap.meetsConstraint(i, edge, nameMap)) {
      mark(edge, i, j, forward);
      markReachable((forward ? edge.getTarget() : edge.getSource()),
		    (forward ? j : i), forward, edge);
    }
  }

  /** A set of nodes v<sup>i</sup> in a traversal graph, where the nodes in the
      set are all copies of the same class graph node v with different
      indices i. */
  public class NodeSet extends Traversal.NodeSet {
    NodeSet(Object v) { super(v); indices = new BitSet(copies); }
    BitSet indices;

    /** A list of indices of the nodes in this set. */
    public List getIndices() {
      List list = new ArrayList();
      for (int i = indices.nextSetBit(0); i >= 0; i = indices.nextSetBit(i+1))
	list.add(new Integer(i));
      return list;
    }

    /** Is v<sup>i</sup> in this set? */
    public boolean hasIndex(int i) { return indices.get(i); }

    /** Add index i to this set. */
    void addIndex(int i) { indices.set(i); }

    /** Is this set empty? */
    boolean isEmpty() { return indices.isEmpty(); }

    String indicesToString() { return indices.toString(); }

    public boolean equals(Object o) {
      return super.equals(o) && indices.equals(((NodeSet) o).indices);
    }

    /** The intersection of this node set and ns. */
    NodeSet intersection(NodeSet ns) {
      NodeSet ret = new NodeSet(node);
      ret.indices = (BitSet) indices.clone();
      ret.indices.and(ns.indices);
      return ret;
    }

    /** The union of this node set and ns. */
    NodeSet union(NodeSet ns) {
      NodeSet ret = new NodeSet(node);
      ret.indices = (BitSet) indices.clone();
      ret.indices.or(ns.indices);
      return ret;
    }

    /** A list of EdgeSet objects representing the edges in the
	traversal graph going out of (if outgoing is true) or coming into
	(if outgoing is false) the nodes in this set.  Each EdgeSet will
	be nonempty and have nonempty source and target NodeSets. */
    List getIncidentEdgeSets(boolean outgoing) {
      List edgeSets = new ArrayList();
      if (isEmpty()) return edgeSets;
      Iterator edges;
      try {
	edges = (outgoing
		 ? classGraph.getOutgoingEdges(node)
		 : classGraph.getIncomingEdges(node)).iterator();
      } catch (NoSuchClassGraphNodeException e) {
	return edgeSets;
      }
      while (edges.hasNext()) {
	EdgeI edge = (EdgeI) edges.next();
	EdgeSet es = (EdgeSet) getEdgeSet(edge); // has all copies
	if (es != null) {
	  EdgeSet edgeSet = new EdgeSet(edge);
	  for (int i = 0; i < copies; i++) {
	    if (hasIndex(i)) {
	      Iterator indices = es.getIncidentIndices(i, outgoing).iterator();
	      while (indices.hasNext()) {
		int j = ((Integer) indices.next()).intValue();
		if (outgoing)
		  edgeSet.addIndices(i, j);
		else
		  edgeSet.addIndices(j, i);
	      }
	    }
	  }
	  if (!edgeSet.isEmpty())
	    // FIXME: check for nonempty endpoint NodeSets.
	    edgeSets.add(edgeSet);
	}
      }
      return edgeSets;
    }
  }

  /** A set of edges u^i <code>-l-&gt;</code> v^j in a traversal graph, where the
      edges in the set are all copies of the same class graph edge
      u <code>-l-&gt;</code> v with different endpoint indices i and j. */
  public class EdgeSet extends Traversal.EdgeSet {
    EdgeSet(EdgeI e) {
      super(e);
      indices = new BitSet(copies);
      indexPairs = new LinkedHashSet();
    }
    BitSet indices;
    Set indexPairs;

    /** An unmodifiable Set of IndexPair objects representing the
        endpoint indices of the intercopy copies in this set, i.e. the
        set of all (i,j) such that i != j and u^i <code>-l-&gt;</code> v^j is in the
        set. */
    public Set getIntercopyIndices() {
      return Collections.unmodifiableSet(indexPairs);
    }

    /** Is u^i <code>-l-&gt;</code> v^j in this set? */
    public boolean hasIndices(int i, int j) {
      return i == j ? indices.get(i) : indexPairs.contains(new IndexPair(i,j));
    }

    /** An unmodifiable list of target indices (Integer objects)
	corresponding to source index i. */
    public List getTargetIndices(int i) {
      return Collections.unmodifiableList(getIncidentIndices(i, true));
    }

    /** An unmodifiable list of source indices (Integer objects)
	corresponding to target index j. */
    public List getSourceIndices(int j) {
      return Collections.unmodifiableList(getIncidentIndices(j, false));
    }

    /** A list of indices (Integer objects) corresponding to the other
	end of index i, which is the source if source is true. */
    List getIncidentIndices(int i, boolean source) {
      List list = new ArrayList();
      if (isEmpty()) return list;
      if (indices.get(i)) list.add(new Integer(i));
      // FIXME: maybe keep two hashtables, one for each direction.
      Iterator ips = indexPairs.iterator();
      while (ips.hasNext()) {
	IndexPair ip = (IndexPair) ips.next();
	if ((source ? ip.getSource() : ip.getTarget()) == i) {
	  list.add(new Integer(source ? ip.getTarget() : ip.getSource()));
	}
      }
      return list;
    }

    /** The set of target nodes of edges in this set. */
    public Traversal.NodeSet getTargetNodeSet() {
      NodeSet nodes = new NodeSet(edge.getTarget());
      for (int i = 0; i < copies; i++) if (indices.get(i)) nodes.addIndex(i);
      Iterator ips = indexPairs.iterator();
      while (ips.hasNext()) {
	IndexPair ip = (IndexPair) ips.next();
	nodes.addIndex(ip.getTarget());
      }
      return nodes;
    }

    /** Add u^i <code>-l-&gt;</code> v^j to this set. */
    void addIndices(int i, int j) {
      if (i == j) indices.set(i); else indexPairs.add(new IndexPair(i,j));
    }

    /** Is this set empty? */
    boolean isEmpty() { return indices.isEmpty() && indexPairs.isEmpty(); }

    String indicesToString() { 
      return indices +
	(indexPairs.isEmpty() ? "" : " intercopy: " + indexPairs);
    }

    public boolean equals(Object o) {
      return super.equals(o)
	&& indices.equals(((EdgeSet) o).indices)
	&& indexPairs.equals(((EdgeSet) o).indexPairs);
    }
  }

  /** A pair of indices, representing the copy indices on the source
      and target of an edge in the traversal graph. */
  public class IndexPair {
    protected int source, target;
    IndexPair(int i, int j) { source = i; target = j; }
    /** The copy index of the source of the edge. */
    public int getSource() { return source; }
    /** The copy index of the target of the edge. */
    public int getTarget() { return target; }
    public boolean equals(Object ip) {
      return (ip instanceof IndexPair
	      && ((IndexPair) ip).source == source
	      && ((IndexPair) ip).target == target);
    }
    public int hashCode() {
      return copies * source + target;
    }
    public String toString() {
      return source + " -> " + target;
    }
  }

  /** Keep track of the marks for a node by keeping three NodeSet
      objects, one for each direction and one for the intersection. */
  class NodeSets {
    NodeSet forw, back, both;
    NodeSets(Object v) {
      forw = new NodeSet(v);
      back = new NodeSet(v);
      both = new NodeSet(v);
    }
    boolean hasIndex(int i, boolean forward) {
      return (forward ? forw : back).hasIndex(i);
    }
    void addIndex(int i, boolean forward) {
       (forward ? forw : back).addIndex(i);
    }
    boolean hasIndex(int i) { return both.hasIndex(i); }
    void addIndex(int i) { both.addIndex(i); }
    NodeSet getNodeSet() { return both.isEmpty() ? null : both; }
  }

  /** Keep track of the marks for an edge by keeping three EdgeSet
      objects, one for each direction and one for the intersection. */
  class EdgeSets {
    EdgeSet forw, back, both;
    EdgeSets(EdgeI e) {
      forw = new EdgeSet(e);
      back = new EdgeSet(e);
      both = new EdgeSet(e);
    }
    boolean hasIndices(int i, int j, boolean forward) {
      return (forward ? forw : back).hasIndices(i, j);
    }
    void addIndices(int i, int j, boolean forward) {
       (forward ? forw : back).addIndices(i, j);
    }
    boolean hasIndices(int i, int j) { return both.hasIndices(i, j); }
    void addIndices(int i, int j) { both.addIndices(i, j); }
    EdgeSet getEdgeSet() { return both.isEmpty() ? null : both; }
  }

  /** A map from nodes to NodeSets objects. */
  LinkedHashMap nodes = new LinkedHashMap();
  /** A map from strings (edge keys) to EdgeSets objects. */
  LinkedHashMap edges = new LinkedHashMap();

  /** Mark node v<sup>i</sup>, in the forward direction if forward is true,
      otherwise in the backward direction.  Note: this must be idempotent! */
  void mark(Object v, int i, boolean forward) {
    NodeSets sets = (NodeSets) nodes.get(v);
    if (sets == null) nodes.put(v, sets = new NodeSets(v));
    sets.addIndex(i, forward);
    // assumes we do forward before backward...
    if (!forward && sets.hasIndex(i, true)) sets.addIndex(i);
  }

  /** Is node v<sup>i</sup> marked in the forward (backward if forward=false)
      direction? */
  boolean marked(Object v, int i, boolean forward) {
    NodeSets sets = (NodeSets) nodes.get(v);
    return sets != null && sets.hasIndex(i, forward);
  }

  /** Mark edge u^i <code>-l-&gt;</code> v^j (where e = u <code>-l-&gt;</code> v), in the forward
      direction if forward is true, otherwise in the backward
      direction. */
  void mark(EdgeI e, int i, int j, boolean forward) {
    String key = edgeKey(e);
    EdgeSets sets = (EdgeSets) edges.get(key);
    if (sets == null) edges.put(key, sets = new EdgeSets(e));
    sets.addIndices(i, j, forward);
    // assumes we do forward before backward...
    if (!forward && sets.hasIndices(i, j, true)) sets.addIndices(i, j);
  }
    
  /** Is edge u^i <code>-l-&gt;</code> v^j (where e = u <code>-l-&gt;</code> v) marked in the forward
      (backward if forward=false) direction? */
  boolean marked(EdgeI e, int i, int j, boolean forward) {
    EdgeSets sets = (EdgeSets) edges.get(edgeKey(e));
    return sets != null && sets.hasIndices(i, j, forward);
  }

  /** The memoized list of NodeSet objects. */
  List nodesList;

  /** An unmodifiable list of NodeSet objects representing the nodes
      in the traversal graph.
      @see NodeSet */
  public List getNodeSets() {
    if (nodesList == null) {
      nodesList = new ArrayList();
      Iterator i = nodes.values().iterator();
      while (i.hasNext()) {
	NodeSets sets = (NodeSets) i.next();
	NodeSet set = sets.getNodeSet();
	if (set != null) nodesList.add(set);
      }
      nodesList = Collections.unmodifiableList(nodesList);
    }
    return nodesList;
  }

  /** The set of copies of class graph node v in the traversal graph,
      or null if there are none. */
  public Traversal.NodeSet getNodeSet(Object v) {
    NodeSets sets = (NodeSets) nodes.get(v);
    return sets == null ? null : sets.getNodeSet();
  }

  /** The memoized list of EdgeSet objects. */
  List edgesList;
  
  /** An unmodifiable list of EdgeSet objects representing the edges
      in the traversal graph.
      @see EdgeSet */
  public List getEdgeSets() {
    if (edgesList == null) {
      edgesList = new ArrayList();
      Iterator i = edges.values().iterator();
      while (i.hasNext()) {
	EdgeSets sets = (EdgeSets) i.next();
	EdgeSet set = sets.getEdgeSet();
	if (set != null) edgesList.add(set);
      }
      edgesList = Collections.unmodifiableList(edgesList);
    }
    return edgesList;
  }

  /** The set of copies of the class graph edge with the given key in
      the traversal graph, or null if there are none. */
  public Traversal.EdgeSet getEdgeSet(String key) {
    EdgeSets sets = (EdgeSets) edges.get(key);
    return sets == null ? null : sets.getEdgeSet();
  }

  /** A map from class graph nodes to NodeSet objects representing the
      set of start tokens for that node. */
  LinkedHashMap startSets = new LinkedHashMap();

  /** A map from class graph nodes to NodeSet objects representing the
      set of finish tokens for that node. */
  LinkedHashMap finishSets = new LinkedHashMap();

  /** Compute the set of start nodes in the traversal graph:
      T<sub>s</sub> is the set of nodes v such that
      s<sup>*</sup> -&gt; v is an edge in G''.
  */
  void makeStartSet() throws TraversalException {
    makeEndpointSet(startSets, sourceNodeSets.values());
  }

  /** Compute the set of finish nodes in the traversal graph:
      T<sub>f</sub> is the set of nodes v such that
      v -&gt; t<sup>*</sup> is an edge in G''.
  */
  void makeFinishSet() throws TraversalException {
    makeEndpointSet(finishSets, targetNodeSets.values());
  }

  void makeEndpointSet(Map endpointSets, Collection nodeSets) {
    Iterator it = nodeSets.iterator();
    while (it.hasNext()) {
      NodeSet set = (NodeSet) it.next();
      Object v = set.getNode();
      NodeSet setInTG = (NodeSet) getNodeSet(v);
      if (setInTG != null) {
	setInTG = setInTG.intersection(set);
	NodeSet endpointSet = (NodeSet) endpointSets.get(v);
	if (endpointSet == null) {
	  endpointSet = setInTG;
	} else {
	  endpointSet = endpointSet.union(setInTG);
	}
	endpointSets.put(v, endpointSet);
      }
    }
  }

  /** The memoized start set. */
  List startSet;
  /** The memoized finish set. */
  List finishSet;

  public List getStartSet() {
    if (startSet == null) {
      startSet = new ArrayList();
      Iterator i = startSets.values().iterator();
      while (i.hasNext()) {
	NodeSet set = (NodeSet) i.next();
	if (!set.isEmpty()) startSet.add(set);
      }
      startSet = Collections.unmodifiableList(startSet);
    }
    return startSet;
  }

  public Traversal.NodeSet getStartSet(Object v) {
    NodeSet set = (NodeSet) startSets.get(v);
    return (set == null || set.isEmpty()) ? null : set;
  }

  public List getFinishSet() {
    if (finishSet == null) {
      finishSet = new ArrayList();
      Iterator i = finishSets.values().iterator();
      while (i.hasNext()) {
	NodeSet set = (NodeSet) i.next();
	if (!set.isEmpty()) finishSet.add(set);
      }
      finishSet = Collections.unmodifiableList(finishSet);
    }
    return finishSet;
  }

  public Traversal.NodeSet getFinishSet(Object v) {
    NodeSet set = (NodeSet) finishSets.get(v);
    return (set == null || set.isEmpty()) ? null : set;
  }

  /** A string representation of the graph.  Print nodes and edges in
      each copy of the graph, along with edges between copies. */
  public String toString() {
    String s[][] = new String[copies][copies+1];
    for (int i = 0; i < copies; i++) {
      s[i][0] = "Copy " + i + ":\n";
      s[i][0] += " Nodes:\n";
      for (int j = 0; j < copies; j++) {
	s[i][j+1] = "";
      }
    }
    Iterator nodeSets = getNodeSets().iterator();
    while (nodeSets.hasNext()) {
      NodeSet nodeSet = (NodeSet) nodeSets.next();
      for (int i = 0; i < copies; i++) {
	if (nodeSet.hasIndex(i)) {
	  s[i][0] += " " + nodeSet.getNode() + "\n";
	}
      }
    }
    for (int i = 0; i < copies; i++) {
      s[i][0] += " Edges:\n";
    }
    Iterator edgeSets = getEdgeSets().iterator();
    while (edgeSets.hasNext()) {
      EdgeSet edgeSet = (EdgeSet) edgeSets.next();
      String edge = edgeKey(edgeSet.getEdge());
      for (int i = 0; i < copies; i++) {
	if (edgeSet.hasIndices(i, i)) {
	  s[i][0] += " " + edge + "\n";
	}
      }
      Iterator ici = edgeSet.getIntercopyIndices().iterator();
      while (ici.hasNext()) {
	IndexPair ip = (IndexPair) ici.next();
	s[ip.getSource()][ip.getTarget()+1] +=
	  " " + ip.getTarget() + ": " + edge + "\n";
      }
    }
    for (int i = 0; i < copies; i++) {
      s[i][0] += " Edges to other copies:\n";
    }
    String ss = "";
    for (int i = 0; i < copies; i++) {
      for (int j = 0; j < copies+1; j++) {
	ss += s[i][j];
      }
    }
    return "Start set: " + getStartSet() + "\n"
      + ss + "Finish set: " + getFinishSet();
  }
}