package org.eclipse.emf.henshin.sam.invcheck.algorithm;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Stack;
import java.util.Vector;

import org.eclipse.emf.common.util.BasicEList;
import org.eclipse.emf.common.util.EList;
import org.eclipse.emf.henshin.sam.invcheck.InvariantCheckerUtil;
import org.eclipse.emf.henshin.sam.invcheck.SubgraphIterator;
import org.eclipse.emf.henshin.sam.invcheck.adapter.GCNACAdapter;
import org.eclipse.emf.henshin.sam.invcheck.adapter.SamGraphInvCheckGraphAdapter;
import org.eclipse.emf.henshin.sam.invcheck.algorithm.IsomorphicPartPartialMatcher.MatchingState.BackTrackReason;
import org.eclipse.emf.henshin.sam.invcheck.algorithm.IsomorphicPartPartialMatcher.MatchingState.MatchingOperation;
import org.eclipse.emf.henshin.sam.invcheck.filter.RuleApplicationFilter;
import org.eclipse.emf.henshin.sam.invcheck.nac.GraphWithNacs;
import org.eclipse.emf.henshin.sam.invcheck.nac.MatchWithNacs;
import org.eclipse.emf.henshin.sam.invcheck.nac.NacFactory;
import org.eclipse.emf.henshin.sam.invcheck.nac.NegativeApplicationCondition;
import org.eclipse.emf.henshin.sam.model.samannotation.AnnotatedElem;
import org.eclipse.emf.henshin.sam.model.samannotation.Annotation;
import org.eclipse.emf.henshin.sam.model.samgraph.Edge;
import org.eclipse.emf.henshin.sam.model.samgraph.Graph;
import org.eclipse.emf.henshin.sam.model.samgraph.Node;
import org.eclipse.emf.henshin.sam.model.samgraph.SamgraphPackage;
import org.eclipse.emf.henshin.sam.model.samrules.RuleGraph;
import org.eclipse.emf.henshin.sam.model.samrules.SamrulesPackage;
import org.eclipse.emf.henshin.sam.model.samtrace.Match;
import org.eclipse.emf.henshin.sam.model.samtrace.SamtraceFactory;
import org.eclipse.emf.henshin.sam.model.samtypegraph.EdgeDirection;
import org.eclipse.emf.henshin.sam.model.samtypegraph.EdgeType;
import org.eclipse.emf.henshin.sam.model.samtypegraph.NodeType;

/**
 * Finds matchings between a set of graph items (current subgraph) and a host
 * graph. <br>
 * <br>
 * Is used six times: <br>
 * <ul>
 * <li>To find intersections between the right part of a rule and a
 * <a href="../../../../../doc/glossary.html">forbidden property</a> in order to
 * construct a counterexample. ({@link MatchSubgprahFilter})</li>
 * <li>To translate NACs from a forbidden subgraph to a
 * <a href="../../../../../doc/glossary.html">merged graph</a> when constructing
 * a counterexample. ({@link NACTranslator})</li>
 * <li>To ensure the applicability of a rule to a
 * <a href="../../../../../doc/glossary.html">source graph pattern</a>. (
 * {@link RuleApplicationFilter})</li>
 * <li>To find a forbidden property in a source graph pattern. (
 * {@link HybridPropertyFilter})</li>
 * <li>To find the left part of a higher-priority rule in a source graph
 * pattern. ({@link HybridGraphRuleFilter})</li>
 * <li>To find the left part of an urgent rule in a
 * <a href="../../../../../doc/glossary.html">target graph pattern</a>. (
 * {@link HybridUrgentGraphRuleFilter})</li>
 * </ul>
 * <br>
 * The IPM matches only positive components. When matching NACs, separate IPM
 * instances are launched and filled with positive representations of the NACs.
 * <br>
 * <br>
 * The IPM can be executed in different modes: <br />
 * <dl>
 * <dt>MATCH_CALLs</dt>
 * <dd>try to match the current subgraph to the host graph. NACs are matched
 * with separate NAC_MATCH_CALLs.</dd>
 * <dt>NAC_MATCH_CALLs</dt>
 * <dd>try to match the current subgraph (being the positive representation of a
 * NAC including its positive interface) to the positive representation of its
 * NAC counterpart (host graph).</dd>
 * <dt>CHECK_NAC_CALLs</dt>
 * <dd>try to find a NAC (its positive representation, to be exact) as positive
 * part in the host graph after the NAC has been matched to another NAC. Finding
 * such a positive occurrence of a NAC would obviously result in failure of the
 * current matching process.</dd>
 * <dt>NAC_TRANSLATION_CALLs</dt>
 * <dd>find all partial matchings of the positive representation of a NAC
 * (current subgraph) in a merged graph (host graph). If the NAC can be matched
 * completely, the result will be empty.</dd>
 * </dl>
 * 
 * @author jfd
 */
public class IsomorphicPartPartialMatcher implements AlgorithmComponent {

	private static class MatchingStateFactory {

		/**
		 * The checkNodesStates array stores all available
		 * <code>MatchingStates</code> for checking nodes.
		 */
		private MatchingState[] checkNodeStates;

		/**
		 * the index of the next CHECK_NODE <code>MatchingState</code>.
		 */
		private int checkNodeStatesIndex = 0;

		/**
		 * The checkEdgeStates array stores all available
		 * <code>MatchingStates</code> for checking edges.
		 */
		private MatchingState[] checkEdgeStates;

		/**
		 * the index of the next CHECK_EDGE <code>MatchingState</code>.
		 */
		private int checkEdgeStatesIndex = 0;

		/**
		 * Initializes the factory with the specified number of
		 * <code>MatchingStates</code> for node and edge matching operations,
		 * respectively.
		 * 
		 * @param non
		 *            number of <code>MatchingStates</code> to create for
		 *            matching <code>Nodes</code>.
		 * @param noe
		 *            number of <code>MatchingStates</code> to create for
		 *            matching <code>Edges</code>.
		 */
		public MatchingStateFactory(final int non, final int noe) {
			checkNodeStates = new MatchingState[non];
			checkEdgeStates = new MatchingState[noe];
			checkNodeStatesIndex = non - 1;
			checkEdgeStatesIndex = noe - 1;
			for (int i = 0; i < non; i++) {
				checkNodeStates[i] = new MatchingState(MatchingOperation.CHECK_NODE);
			}
			for (int i = 0; i < noe; i++) {
				checkEdgeStates[i] = new MatchingState(MatchingOperation.CHECK_EDGE);
			}
		}

		/**
		 * Same as <code>new MatchingStateFactory(n,n)</code>
		 * 
		 * @see MatchingStateFactory#MatchingStateFactory(int, int)
		 * @param n
		 */
		public MatchingStateFactory(final int n) {
			this(n, n);
		}

		/**
		 * Same as <code>new MatchingStateFactory(20,20);</code>
		 * 
		 * @see MatchingStateFactory#MatchingStateFactory(int, int)
		 */
		public MatchingStateFactory() {
			this(20, 20);
		}

		/**
		 * Returns a new <code>MatchingState</code> for checking
		 * <code>Nodes</code>.<br />
		 * If the factory's internal array still contains a
		 * <code>MathcingState</code> this one is returned. A new one will be
		 * created, otherwise.
		 * 
		 * @return a <code>MatchingState</code> for matching <code>Nodes</code>.
		 */
		public MatchingState getCheckNodeState() {
			MatchingState result;
			if (checkNodeStatesIndex >= 0) {
				result = checkNodeStates[checkNodeStatesIndex];
				checkNodeStates[checkNodeStatesIndex] = null;
				checkNodeStatesIndex--;
				cleanMatchingState(result);
			} else {
				result = new MatchingState(MatchingOperation.CHECK_NODE);
			}
			return result;
		}

		/**
		 * Returns a new <code>MatchingState</code> for checking
		 * <code>Edges</code>.<br />
		 * If the factory's internal array still contains a
		 * <code>MathcingState</code> this one is returned. A new one will be
		 * created, otherwise.
		 * 
		 * @return a <code>MatchingState</code> for matching <code>Edges</code>.
		 */
		public MatchingState getCheckEdgeState() {
			MatchingState result;
			if (checkEdgeStatesIndex >= 0) {
				result = checkEdgeStates[checkEdgeStatesIndex];
				checkEdgeStates[checkEdgeStatesIndex] = null;
				checkEdgeStatesIndex--;
				cleanMatchingState(result);
			} else {
				result = new MatchingState(MatchingOperation.CHECK_EDGE);
			}
			return result;
		}

		public void releaseMatchingState(MatchingState ms) {
			switch (ms.matchOp) {
			case CHECK_NODE:
				if (checkNodeStatesIndex < checkNodeStates.length - 1) {
					checkNodeStatesIndex++;
					checkNodeStates[checkNodeStatesIndex] = ms;
				}
				break;
			case CHECK_EDGE:
				if (checkEdgeStatesIndex < checkEdgeStates.length - 1) {
					checkEdgeStatesIndex++;
					checkEdgeStates[checkEdgeStatesIndex] = ms;
				}
				break;
			}
		}

		private void cleanMatchingState(MatchingState ms) {
			ms.backtrack = BackTrackReason.NONE;
			ms.currentEdge = null;
			ms.currentNode = null;
			ms.edgeIterator = null;
			ms.mappedEdgeIterator = null;
			ms.mappedToNode = null;
		}
	}

	/**
	 * The graph the current subgraph will be matched to.
	 */
	private Graph hostGraph;

	/**
	 * A set of graph items representing the current subgraph to be matched to
	 * the host graph.
	 */
	private Set<AnnotatedElem> currentSubGraph;

	/**
	 * The data structure controlling the execution and order of the matching
	 * process.
	 */
	private Stack<MatchingState> stack = new Stack<MatchingState>();

	/**
	 * A data structure storing the node matching, edge matching and NAC
	 * matching the matcher has currenty built.
	 */
	private MatchWithNacs currentMatching;

	/**
	 * The order of the matching process for the current graphs.
	 */
	private LinkedList<MatchingState> matchingHistory = new LinkedList<MatchingState>();

	/**
	 * Stores the match mode that is currently active to control the way the
	 * matchers works.
	 */
	private MatchMode mode = MatchMode.MATCH_CALL;

	/**
	 * A list storing one matching for each matching step. Is used only within a
	 * NAC translation call.
	 */
	private LinkedList<MatchWithNacs> iterativeMatchings = new LinkedList<MatchWithNacs>();

	/**
	 * A list preventing certain edges from being tried as "mapped" edges when
	 * executing a NAC translation call.
	 */
	private List<Edge> blacklist = new LinkedList<Edge>();

	/**
	 * A list preventing certain nodes from being tried as "mapped" edges when
	 * executing a NAC translation call.
	 */
	private List<Node> nodeBlacklist = new LinkedList<Node>();

	/**
	 * Stores the node degrees of the current subgraph's nodes.
	 */
	private Map<Node, Integer> nodeDegrees;

	/**
	 * Stores the number of types in the host graph
	 */
	private Map<NodeType, Integer> typeCount;

	/**
	 * Saves the nacs in the subgraph
	 */
	private Set<NegativeApplicationCondition> nacs = null;

	/**
	 * Iterates over the nacs in the subgraph
	 */
	private Iterator<NegativeApplicationCondition> nacIterator = null;

	/**
	 * Only used in nac match call or nac translation call.
	 */
	private Match nacInterfaceMatch = null;

	/**
	 * Gets the graph or pattern the current subgraph will be matched to.
	 *
	 * @return The host graph
	 */
	public Graph getHostGraph() {
		return this.hostGraph;
	}

	/**
	 * Sets the graph or pattern the current subgraph will be matched to and
	 * calculates the number of each node type.
	 *
	 * @param value
	 *            The new host graph
	 */
	public void setHostGraph(final Graph value) {
		this.hostGraph = value;
		this.typeCount = calculateTypeCount();
	}

	/**
	 * Calculates the type count.
	 */
	private Map<NodeType, Integer> calculateTypeCount() {
		Map<NodeType, Integer> result = new HashMap<NodeType, Integer>();
		if (this.hostGraph == null) {
			return result;
		}
		for (Node n : this.hostGraph.getNodes()) {
			NodeType type = n.getInstanceOf();
			if (result.containsKey(type)) {
				result.put(type, result.get(type) + 1);
			} else {
				result.put(type, 1);
			}
		}
		return result;
	}

	/**
	 * Indicates a failure to match NACs. New positive matching is required.
	 */
	boolean positiveFailure = false;

	/**
	 * This attribute doesn't represent a GraphRule, it only represents the
	 * right handed side of a GraphRule. More generally speaking, it represents
	 * the graph containing the current subgraph (which might be the same
	 * graph).
	 */
	private Graph pattern;

	/**
	 * Gets the graph containing the current subgraph.
	 *
	 * @return The graph containing the current subgraph
	 */
	public Graph getPattern() {
		return this.pattern;
	}

	/**
	 * Sets the graph containing the current subgraph.
	 *
	 * @param value
	 *            the graph containing the current subgraph
	 */
	public void setPattern(Graph value) {
		this.pattern = value;
	}

	private Iterator<AnnotatedElem> startNodeIter;

	/*
	 * /** This is an experimental field to save matchings where a nac in the
	 * pattern (or a part of its translation to the host, to be more exact) does
	 * not have an equivalent matching NAC in the host. Consequently, the
	 * implication host => pattern cannot be assured as the absence of the nac
	 * in the pattern cannot be assured in the host. We then save the positive
	 * match with the translated NACs for such cases and try to analyse the case
	 * with context generation in another filter. This means, that we treat the
	 * translated unmatched NACs as positive elements (including the original
	 * positive elements) and try to find forbidden patterns (without NACs) in
	 * the graph.
	 * 
	 * (Actually, this is not really necessary. We could also check the
	 * translated elements directly for the forbidden patterns. However, this
	 * would then be part of the IPM which is probably not really desirable.
	 * That is what the next field is for.)
	 */

	/*
	 * private Map<Match, RuleGraph> incompleteNacMatchings; private Set<Graph>
	 * restrictingConstraints;
	 * 
	 * public Map<Match, RuleGraph> getIncompleteMatchings() { return
	 * this.incompleteNacMatchings; }
	 * 
	 * public void setRestrictingConstraint(Set<Graph> restrictingConstraints) {
	 * this.restrictingConstraints = restrictingConstraints; }
	 * 
	 * public void addRestrictingConstraint(Graph restrictingConstraint) { if
	 * (this.restrictingConstraints == null) { this.restrictingConstraints = new
	 * HashSet<Graph>(); }
	 * this.restrictingConstraints.add(restrictingConstraint); }
	 */

	private MatchingStateFactory theFactory;

	/**
	 * A <code>StartConfiguration</code> encapsulates all information that is
	 * required to start the matching of a connected component of the
	 * {@link IsomorphicPartPartialMatcher#currentSubGraph}.
	 * 
	 * @author bb
	 *
	 */
	private static class StartConfiguration {
		/**
		 * the current connected component's start node
		 */
		public Node startNode = null;

		/**
		 * the {@link IsomorphicPartPartialMatcher#matchingHistory
		 * matchingHistories} index at the time this
		 * <code>StartConfiguration</code> has been created.
		 */
		public int historyIndex = 0;

		/**
		 * The <code>Iterator</code> of <code>Nodes</code> contained in the
		 * hostgraph. The <code>Iterator</code> will be reset each time a match
		 * of a previous connected component has to be revoked.
		 */
		public Iterator<Node> hostNodeIter = null;
	}

	private List<StartConfiguration> connectedComponents = null;

	private int connectedComponentIndex = 0;

	/**
	 * Resets this <code>IsomorphicPartMatcher</code> instance.<br />
	 * In particular this method clears the {@link #stack} or creates an empty
	 * one and sets the fields {@link #currentMatching}, {@link #startNode} and
	 * {@link #hostNodeIter} as well as certain flags to null/their default
	 * value.
	 */
	public void reset() {
		if (stack == null) {
			stack = new Stack<MatchingState>();
		} else
			stack.clear();

		if (theFactory == null) {
			theFactory = new MatchingStateFactory();
		}

		if (matchingHistory == null) {
			matchingHistory = new LinkedList<MatchingState>();
		} else {
			for (MatchingState ms : matchingHistory) {
				theFactory.releaseMatchingState(ms);
			}
			matchingHistory.clear();
		}

		if (connectedComponents == null) {
			this.connectedComponents = new ArrayList<StartConfiguration>();
		} else {
			this.connectedComponents.clear();
		}
		this.connectedComponents.add(new StartConfiguration());
		this.connectedComponentIndex = 0;

		this.iterativeMatchings.clear();
		this.currentMatching = null;
		this.nodeDegrees = null;
		this.startNodeIter = null;
		this.blacklist.clear();
		this.nodeBlacklist = null;
		this.nacIterator = null;
		this.nacs = null;
		this.positiveFailure = false;
		this.nacInterfaceMatch = null;
	}

	private void addFirstCheckNACState() {
		// if there is an check edge state with currentEdge == null, remove this
		// entry
		if (stack.size() > 0) {
			if (stack.peek().matchOp == MatchingOperation.CHECK_EDGE && stack.peek().backtrack == BackTrackReason.NONE
					&& stack.peek().currentEdge == null) {
				stack.pop();
			}
		}

		if (nacs == null) {
			nacs = new HashSet<NegativeApplicationCondition>();
			for (AnnotatedElem gI : currentSubGraph) {
				if (SamgraphPackage.eINSTANCE.getEdge().isSuperTypeOf(gI.eClass())) {
					if (InvariantCheckerUtil.isNegated((Edge) gI)) {
						Edge e = (Edge) gI;
						NegativeApplicationCondition nac = GCNACAdapter
								.getInstance(InvariantCheckerUtil.getHighestCondition(e));
						nacs.add(nac);
					}
				} else {
					if (InvariantCheckerUtil.isNegated((Node) gI)) {
						Node n = (Node) gI;
						NegativeApplicationCondition nac = GCNACAdapter
								.getInstance(InvariantCheckerUtil.getHighestCondition(n));
						nacs.add(nac);
					}
				}
			}
		}
		nacIterator = nacs.iterator();
		MatchingState ms = new MatchingState(MatchingOperation.CHECK_NAC);
		ms.currentNAC = nacIterator.next();
		stack.push(ms);
	}

	/**
	 * Returns the next matching for the actual values of: {@link #pattern},
	 * {@link #hostGraph} and {@link #currentSubGraph}.<br />
	 * <p>
	 * The first invocation of this method after {@link #reset()} has been
	 * invoked, initializes the <code>IsomorphicPartMatcher</code>'s internal
	 * bookkeeping and returns the first matching of the
	 * {@link #currentSubGraph| current subgraph} in the {@link #hostGraph| host
	 * graph}. Following invocations invalidate the last matched element and
	 * start a backtracking procedure to find the next matching. If no more
	 * matching could be found the method returns <code>null</code>
	 * </p>
	 * The execution of this method might create additional instances of the
	 * matcher and execute them.
	 * <p>
	 * elements from the {@link #pattern| graph pattern} are returned as the
	 * keys and elements from the {@link #hostGraph| host graph} are returned as
	 * the values.
	 * </p>
	 * <br>
	 * A matching for a MATCH_CALL or a CHECK_NAC_CALL must fulfill the
	 * following conditions:<br>
	 * <ul>
	 * <li>All nodes from the current subgraph have been matched.</li>
	 * <li>All edges from the current subgraph have been matched.</li>
	 * <li>All NACs from the current subgraph have been matched (by using
	 * separate NAC_MATCH_CALLs).</li>
	 * </ul>
	 * <br>
	 * A matching for a NAC_MATCH_CALL can be correct without having matched all
	 * nodes and edges from the subgraph. This requires that the host graph is
	 * already completely matched so that the subgraph contains more the same,
	 * but more elements and thus is stricter that the host graph.<br>
	 * <br>
	 * Matchings for a NAC_TRANSLATION_CALL are returned as a list of partial
	 * matchings, see {@link #getIterativeMatchings()}.<br>
	 * <br>
	 * If no matching could be found, null will be returned.
	 * 
	 * @return A <code>Match</code> representing a matching of {@link #pattern}
	 *         in {@link #hostGraph} w.r.t to the {@link #currentSubGraph} or
	 *         <code>null</code>.
	 */
	public Match getNextMatching() {

		// When executing a NAC translation call, we only search for partial
		// matches. Thus, the compareTypes method is not applicable in that
		// case.
		if (mode != MatchMode.NAC_TRANSLATION_CALL && !compareTypes(currentSubGraph, hostGraph)) {
			return null;
		}

		if (mode != MatchMode.NAC_TRANSLATION_CALL
				&& posSizeOfSubgraph(currentSubGraph) > this.hostGraph.getEdges().size()
						+ this.hostGraph.getNodes().size()) {
			return null;
		}

		if (mode == MatchMode.MATCH_CALL && numberOfNacs(currentSubGraph) > 0
				&& (hostGraph.eClass() != SamrulesPackage.eINSTANCE.getRuleGraph()
						|| ((RuleGraph) hostGraph).getCondition() == null)) {
			return null;
		}

		MatchingState ms;
		// System.out.println("===");
		boolean reentrantCall = false;
		boolean triedAllHostNodes = false;
		if (this.currentMatching == null) {
			this.currentMatching = NacFactory.eINSTANCE.createMatchWithNacs();
		}
		if (this.theFactory == null) {
			this.theFactory = new MatchingStateFactory();
		}
		if (this.connectedComponents == null) {
			this.connectedComponents = new ArrayList<StartConfiguration>();
			this.connectedComponents.add(new StartConfiguration());
		}
		if (this.currentSubGraph == null) {
			throw new IllegalStateException("initialize the object's current subgraph before invoking getNextMatching");
		} else if (this.nodeDegrees == null) {
			/*
			 * compute the node degrees of the current subgraph's nodes. We
			 * cannot use Node.getIncomingEdge().size() etc. as the this returns
			 * a value that is only valid for the complete pattern. But our
			 * search is restricted to the currentSubgraph attribute and so have
			 * to be the node's degrees.
			 */
			this.nodeDegrees = new HashMap<Node, Integer>(this.currentSubGraph.size());
			for (Iterator<AnnotatedElem> iter = this.currentSubGraph.iterator(); iter.hasNext();) {
				final AnnotatedElem gi = iter.next();
				if (SamgraphPackage.eINSTANCE.getNode().isSuperTypeOf(gi.eClass())) {
					if (!InvariantCheckerUtil.isNegated((Node) gi) && !this.nodeDegrees.containsKey(gi)) {
						this.nodeDegrees.put((Node) gi, 0);
					}
				} else if (!InvariantCheckerUtil.isNegated((Edge) gi)) {
					final Edge edge = (Edge) gi;
					if (this.nodeDegrees.containsKey(edge.getSource())) {
						this.nodeDegrees.put(edge.getSource(), this.nodeDegrees.get(edge.getSource()) + 1);
					} else
						this.nodeDegrees.put(edge.getSource(), 1);
					if (this.nodeDegrees.containsKey(edge.getTarget())) {
						this.nodeDegrees.put(edge.getTarget(), this.nodeDegrees.get(edge.getTarget()) + 1);
					} else
						this.nodeDegrees.put(edge.getTarget(), 1);
				}
			}
		}

		if ((mode == MatchMode.MATCH_CALL || mode == MatchMode.NAC_MATCH_CALL)
				&& (this.stack != null && this.stack.size() > 0)) {
			/*
			 * The method is invoked after a previous match has been found.
			 * Thus, we invalidate the stack's topmost entry, to start the
			 * matcher's backtracking functionality. This is only applicable
			 * when executing a match call (as for example when executing the
			 * MatchSubgraphFilter).
			 */
			reentrantCall = true;
			handleReentrantCall();
		}

		/*
		 * The matching process will continue while there are unmatched nodes,
		 * edges or NACs in the current subgraph. The process may end
		 * prematurely in the case of a NAC match call when the host graph is
		 * found to be a stricter NAC.
		 */
		while ((reentrantCall
				|| (((InvariantCheckerUtil.positiveSize(this.currentMatching) < posSizeOfSubgraph(currentSubGraph))
						|| (this.currentMatching.getNacMatching().size() < numberOfNacs(currentSubGraph)))
						&& (triedAllHostNodes == false)))) {

			if (!reentrantCall && mode == MatchMode.MATCH_CALL
					&& InvariantCheckerUtil.positiveSize(this.currentMatching) == posSizeOfSubgraph(currentSubGraph)
					&& numberOfNacs(currentSubGraph) > 0) {
				if (nacIterator == null && !positiveFailure) {
					// positive matching is complete, build first check nac
					// state
					addFirstCheckNACState();
				}
				if (positiveFailure) {
					positiveFailure = false;
				}
			}
			reentrantCall = false;

			if (stack.size() > 0) {
				ms = stack.peek();
				// if (mode != MatchMode.NAC_TRANSLATION_CALL || mode ==
				// MatchMode.NAC_MATCH_CALL) {
				// System.out.println("now checking: " + ms.toString() + " " +
				// ms.backtrack);
				// }

				switch (ms.matchOp) {
				case CHECK_NODE:
					checkNode(ms);
					break;
				case CHECK_EDGE:
					checkEdge(ms);
					break;
				case CHECK_NAC:
					checkNAC();
					break;
				}
			} else {
				// Stack is empty, mode is MATCH_CALL, NAC_MATCH_CALL or
				// NAC_TRANSLATION_CALL.
				// Have to find an initial node.
				// Will happen in two cases: 1) first call of gNM for a specific
				// subgraph or 2) stack has been completely removed because of
				// backtracking.
				triedAllHostNodes = createInitialNodePair();
				if (triedAllHostNodes && connectedComponentIndex > 0) {
					for (int i = connectedComponents
							.get(connectedComponentIndex - 1).historyIndex; i < connectedComponents
									.get(connectedComponentIndex).historyIndex; i++) {
						if (i < matchingHistory.size())
							stack.push(matchingHistory.get(i));
					}
					stack.peek().backtrack = BackTrackReason.FAILURE;
					this.connectedComponentIndex--;
					triedAllHostNodes = false;
				}
				if (this.connectedComponents.get(connectedComponentIndex).startNode == null) {
					return null;
				}
			}
		}
		return triedAllHostNodes ? null : this.currentMatching.copy();
	}

	/**
	 * This method determines the number of NACs contained in the given
	 * subgraph.
	 * 
	 * @param currentSubGraph
	 *            the graph whose NACs will be counted
	 * @return the number of NACs
	 */
	private int numberOfNacs(Set<AnnotatedElem> currentSubGraph) {
		Set<NegativeApplicationCondition> nacs = new HashSet<NegativeApplicationCondition>();
		for (AnnotatedElem gI : currentSubGraph) {
			if (SamgraphPackage.eINSTANCE.getEdge().isSuperTypeOf(gI.eClass())) {
				if (InvariantCheckerUtil.isNegated((Edge) gI)) {
					Edge e = (Edge) gI;
					NegativeApplicationCondition nac = GCNACAdapter
							.getInstance(InvariantCheckerUtil.getHighestCondition(e));
					nacs.add(nac);
				}
			} else {
				if (InvariantCheckerUtil.isNegated((Node) gI)) {
					Node n = (Node) gI;
					NegativeApplicationCondition nac = GCNACAdapter
							.getInstance(InvariantCheckerUtil.getHighestCondition(n));
					nacs.add(nac);
				}
			}
		}
		return nacs.size();
	}

	/**
	 * This method determines the number of positive graph items in a given
	 * subgraph.
	 * 
	 * @param currentSubGraph
	 *            the subgraph whose positive items will be counted
	 * @return the number of positive items
	 */
	private int posSizeOfSubgraph(Set<AnnotatedElem> currentSubGraph) {
		int count = 0;
		for (AnnotatedElem gI : currentSubGraph) {
			if (SamgraphPackage.eINSTANCE.getEdge().isSuperTypeOf(gI.eClass())) {
				if (!InvariantCheckerUtil.isNegated((Edge) gI)) {
					count++;
				}
			} else {
				if (!InvariantCheckerUtil.isNegated((Node) gI)) {
					count++;
				}
			}
		}
		return count;
	}

	/**
	 * This method creates an arbitrary pair of two nodes and pushes an
	 * corresponding {@link MatchingState} instance onto the {@link #stack}.
	 * <br />
	 * If the {@link #startNode} field is empty the {@link #currentSubGraph}'s
	 * first node is selected. The {@link #startNode} is then tried to match to
	 * the {@link #hostGraph}'s next {@link Node}.
	 * 
	 * @return <code>false</code> if the {@link #hostGraph} has unvisited nodes.
	 *         <code>true></code> otherwise.
	 */
	private boolean createInitialNodePair() {
		// System.out.println("createInitialNodePair");
		boolean triedAllHostNodes;
		if (this.currentMatching.getSize() > this.connectedComponents.get(connectedComponentIndex).historyIndex
				&& this.currentMatching.getSize() < this.currentSubGraph.size()) {
			this.connectedComponentIndex++;
			if (this.connectedComponents.size() > this.connectedComponentIndex) {
				this.connectedComponents.get(this.connectedComponentIndex).hostNodeIter = null;
			} else {
				final StartConfiguration tmpConf = new StartConfiguration();
				tmpConf.historyIndex = this.currentMatching.getSize();
				tmpConf.startNode = null;
				tmpConf.hostNodeIter = null;
				this.connectedComponents.add(tmpConf);
			}
		}

		if (this.connectedComponents.get(connectedComponentIndex).startNode == null) {
			if (mode == MatchMode.NAC_TRANSLATION_CALL && connectedComponentIndex == 0) {
				return true;
			}
			findStartNode();
		}
		if (this.connectedComponents.get(connectedComponentIndex).hostNodeIter == null) {
			this.connectedComponents.get(connectedComponentIndex).hostNodeIter = this.hostGraph.getNodes().iterator();
		}
		Node next = null;
		triedAllHostNodes = false;
		// iterate through nodes of hostGraph
		// iterator is resetted for each subgraph (input)
		while (this.connectedComponents.get(connectedComponentIndex).hostNodeIter.hasNext() && next == null) {
			next = this.connectedComponents.get(connectedComponentIndex).hostNodeIter.next();
			if (currentMatching.getNodeMatching().containsValue(next) == false) {
				final MatchingState newms = theFactory.getCheckNodeState();
				newms.currentNode = this.connectedComponents.get(connectedComponentIndex).startNode;
				newms.mappedToNode = next;
				// types, negated are not checked, this is done in the checkNode
				// method
				stack.push(newms);
				triedAllHostNodes = false;
			}
		}
		if (next == null) {
			triedAllHostNodes = true;
		}
		return triedAllHostNodes;
	}

	/**
	 * Identifies the first not negative {@link Node} in the
	 * {@link #currentSubGraph}.<br />
	 * This node is not directly returned but the {@link #startNode} field is
	 * accordingly set.
	 */
	private void findStartNode() {
		if (startNodeIter == null) {
			startNodeIter = this.currentSubGraph.iterator();
		}
		while (this.connectedComponents.get(connectedComponentIndex).startNode == null && startNodeIter.hasNext()) {
			AnnotatedElem next = startNodeIter.next();
			if (next instanceof Node && !this.currentMatching.getNodeMatching().containsKey((Node) next)) {
				Node n = (Node) next;
				if (!InvariantCheckerUtil.isNegated(n)) {
					this.connectedComponents.get(connectedComponentIndex).startNode = n;
				}
			}
		}
	}

	/**
	 * This method is invoked if the {@link #getNextMatching()} method is not
	 * invoked the first time.<br />
	 * The method prepares the {@link #stack} to start the backtracking
	 * functionality to find a new matching.
	 * 
	 * Matching has been found and returned, then call of getNextMatching on
	 * same subgraph calls this
	 */
	private void handleReentrantCall() {
		boolean stop = false;
		this.currentMatching.getNacMatching().clear();
		this.nacIterator = null;
		while (this.stack.size() > 0 && !stop) {
			// remove all check nac states.
			if (this.stack.peek().matchOp == MatchingOperation.CHECK_NAC) {
				this.stack.pop();
			} else {
				stop = true;
			}
		}
		if (this.stack.size() > 0 && this.stack.peek().matchOp == MatchingOperation.CHECK_EDGE
				&& this.stack.peek().currentEdge == null) {
			/*
			 * If the last entry of the stack is a CHECK_EDGE entry, but it's
			 * currentEdge field is set to null, this entry has not lead to a
			 * matching and thus has to be removed from the stack.
			 */
			this.stack.pop();
		}
		if (this.stack.size() > 0) {
			// Initiates the backtracking.
			this.stack.peek().backtrack = BackTrackReason.FAILURE;
		}
	}

	public void handleNACMatchCall(Match interfaceMatching, List<Node> interfaceBlacklist) {
		this.nodeBlacklist = interfaceBlacklist;
		mode = MatchMode.NAC_MATCH_CALL;
		this.nacInterfaceMatch = interfaceMatching;
	}

	/**
	 * This method prepares the IPM instance for a NAC translation call,
	 * starting from (negative) nodes that do not belong to the NAC interface.
	 * 
	 * @param startNode
	 *            the start node
	 */
	public void handleNacTranslationCall(Node startNode, List<Edge> edgeBlacklist, List<Node> nodeBlacklist,
			Match nacInterfaceMatch) {

		mode = MatchMode.NAC_TRANSLATION_CALL;
		this.blacklist = edgeBlacklist;
		this.nodeBlacklist = nodeBlacklist;
		this.nacInterfaceMatch = nacInterfaceMatch;

		if (this.currentMatching == null) {
			this.currentMatching = NacFactory.eINSTANCE.createMatchWithNacs();
		}

		this.connectedComponents.get(0).startNode = startNode;

		createInitialNodePair();
		// System.out.println("inner nac translation call: " + startNode);
	}

	/**
	 * This method will handle a CHECK_NODE matching state. It will contain both
	 * the current node (from the current subgraph) and the corresponding
	 * counterpart (to be checked) from the host graph. The nature of the state
	 * might be: <br>
	 * <br>
	 * <dl>
	 * <dt>Failure</dt>
	 * <dd>Remove the current matching state from the stack. Remove both nodes
	 * from the current matching. Set the nature of the previous state to
	 * failure.</dd>
	 * <dt>Backtrack</dt>
	 * <dd>Remove the current matching state from the stack. Set the nature of
	 * the previous state to backtrack unless the IPM executes a NAC_MATCH_CALL
	 * or a CHECK_NAC_CALL.</dd>
	 * <dt>None</dt>
	 * <dd>Check {@link #degreePredicate(Node, Node)},
	 * {@link #negatedPredicate(Node, Node)} and
	 * {@link #typePredicate(Node, Node)} for the current nodes. If successful,
	 * add the nodes to the current matching and add a new CHECK_EDGE matching
	 * state to the stack. Otherwise remove the current matching state from the
	 * stack and set the previous state to failure.</dd>
	 * </dl>
	 * <br>
	 * A CHECK_NODE state usually results from a successfully handled CHECK_EDGE
	 * state. It is also the first matching state on the stack when executing a
	 * MATCH_CALL.
	 * 
	 * @param ms
	 *            the current matching state
	 */
	private void checkNode(final MatchingState ms) {
		if (ms.backtrack == BackTrackReason.FAILURE) {
			// Remove wrong/invalid matchingState from stack.
			stack.pop();
			this.currentMatching.getNodeMatching().remove(ms.currentNode);
			this.matchingHistory.remove(ms);
			theFactory.releaseMatchingState(ms);

			if (stack.size() > 0) {
				// If the node matching is invalid, the edge matching leading to
				// it has to be removed, too.
				final MatchingState tmpMS = stack.peek();
				tmpMS.backtrack = BackTrackReason.FAILURE;
			}
		} else if (ms.backtrack == BackTrackReason.BACKTRACK) {
			// backtracking, remove stack until another chance can be found
			stack.pop();
			if (stack.size() > 0) {
				stack.peek().backtrack = BackTrackReason.BACKTRACK;
			}
		} else {
			// check predicates, build new checkEdge state if applicable
			final Node expectedNode = ms.currentNode;
			final Node foundNode = ms.mappedToNode;
			if (nacInterfaceNodePredicate(expectedNode, foundNode) && degreePredicate(foundNode, expectedNode)
					&& typePredicate(expectedNode, foundNode) && negatedPredicate(expectedNode, foundNode)
					&& ((!currentMatching.getNodeMatching().containsKey(expectedNode)
							&& !currentMatching.getNodeMatching().containsValue(foundNode))
							|| (foundNode == currentMatching.getNodeMatching().get(expectedNode)))) {
				this.currentMatching.getNodeMatching().put(expectedNode, foundNode);
				this.matchingHistory.add(ms);
				if (this.mode == MatchMode.NAC_TRANSLATION_CALL) {
					iterativeMatchings.add(currentMatching.copy());
				}
				MatchingState newms = theFactory.getCheckEdgeState();
				newms.currentNode = expectedNode;
				newms.mappedToNode = foundNode;
				newms.currentNAC = ms.currentNAC;
				newms.mappedToNAC = ms.mappedToNAC;
				stack.push(newms);
				// next call should be checkEdge
			} else {
				// cannot match nodes, remove from stack
				// next call should be checkEdge
				stack.pop();
				if (stack.size() > 0) {
					stack.peek().backtrack = BackTrackReason.FAILURE;
				}
			}
		}
	}

	/**
	 * Returns an unmatched edge in the current subgraph that leads to or comes
	 * from the current node in the matching state. This method will try to
	 * return positive edges first.
	 * 
	 * An edge will be returned if it fulfills all of the following conditions:
	 * <ul>
	 * <li>It is not contained in the current matching, thus being unmatched
	 * </li>
	 * <li>It is contained in the edgeIterator of the current matching state,
	 * which iterates over the edges from the currentNode of the current state
	 * </li>
	 * <li>It is contained in the current subgraph (and the pattern)</li>
	 * <li>It is contained in the current subgraph (and the pattern)</li>
	 * </ul>
	 * and additionally fulfills at least one of the following conditions:
	 * <ul>
	 * <li>It is positive (i.e. does not belong to a NAC) and there are
	 * unchecked edges left</li>
	 * <li>It is negative (i.e. belongs to a NAC), all positive edges have been
	 * checked and the <a href="../../../../../doc/glossary.html">positive NAC
	 * interface</a> has been matched</li>
	 * <li>The IPM executes a NAC_TRANSLATION_CALL</li>
	 * </ul>
	 *
	 * When executed the first time, this method will try to return a positive
	 * edge as the matching of NACs currently assumes that the positive NAC
	 * interfaces have already been matched. When all edges have been checked,
	 * the iterator will be reset and the ignoreNegativeEdges flag will be set
	 * to true. When iterating over the edges for the second time, negative
	 * edges will also be checked.
	 * 
	 * @param ms
	 *            the current matching state
	 * @return the unmatched edge
	 */
	private Edge getNextUnmatchedEdge(MatchingState ms) {
		if (ms != null) {
			if (ms.edgeIterator == null) {
				ms.edgeIterator = iteratorOfEdges(ms.currentNode);
			}
			while (ms.edgeIterator.hasNext()) {
				final Edge nextEdge = ms.edgeIterator.next();
				/*
				 * "unmatched", thus not contained in currentMatching but in the
				 * subgraph Only positive edges should be considered.
				 */
				if (this.currentMatching != null && !this.currentMatching.getEdgeMatching().containsKey(nextEdge)
						&& this.currentSubGraph.contains(nextEdge) && !InvariantCheckerUtil.isNegated(nextEdge)) {
					return nextEdge;
				}
			}
		}
		return null;
	}

	/**
	 * This method will handle a CHECK_EDGE matching state. It might contain the
	 * current edge from the current subgraph and might also contain the
	 * corresponding counterpart (which might be checked) from the host graph.
	 * The nature of the state might be: <br>
	 * <br>
	 * <dl>
	 * <dt>Failure</dt>
	 * <dd>If the state is the last state in the matching history, remove it
	 * from the stack and remove both edges from the current matching. Set the
	 * state to NONE so that the next call will try to find a new matching edge.
	 * If not, rebuild the stack. Set the nature of the topmost state to FAILURE
	 * so that the next call will evaluate the states leading to the current
	 * failure.</dd>
	 * <dt>Backtrack</dt>
	 * <dd>If another unmatched edge going from or to the current node can be
	 * found, put it on the stack as a new CHECK_EDGE state. If not, remove the
	 * state from the stack and set the previous state to BACKTRACK in order to
	 * continue the backtracking process.</dd>
	 * <dt>None</dt>
	 * <dd>If the current edge is not set, find one by calling
	 * {@link #getNextUnmatchedEdge(MatchingState)}. Call
	 * {@link #findMatchingEdge(MatchingState)} to find a corresponding
	 * counterpart to the current edge in the host graph. This method will
	 * handle the predicates to be checked.</dd>
	 * </dl>
	 * <br>
	 * When executing a normal (NONE) CHECK_EDGE call, the following scenarios
	 * might occur: <br>
	 * <ul>
	 * <li>A matching edge will be found by
	 * {@link #findMatchingEdge(MatchingState)}. The implications of this will
	 * be explained in said method.</li>
	 * <li>There is no unmatched edge left to be returned by
	 * {@link #getNextUnmatchedEdge(MatchingState)}. The matching state will be
	 * removed from the stack and the previous state will be set to BACKTRACK.
	 * </li>
	 * <li>There was no matching edge to be found and the IPM is in NAC_MATCH
	 * mode. If the host graph NAC is already completely matched, it is stricter
	 * than the NAC in the current subgraph. In that case, the
	 * {@link #stricterNac} flag will be set and the matching process will
	 * terminate in the next iteration of the main loop.</li>
	 * <li>There was no matching edge to be found and the IPM is in
	 * NAC_TRANSLATION mode. As we look for incomplete matching, we cannot
	 * simply return with FAILURE but need to check other edges by using
	 * {@link #getNextUnmatchedEdge(MatchingState)}. If there is an unmatched
	 * edge, a new matching state will be put on the stack. If not, remove the
	 * state from the stack and set the previous state to FAILURE.</li>
	 * <li>There was no matching edge and the IPM is in standard MATCH mode.
	 * Remove the state from the stack and set the prevoius state to FAILURE.
	 * </li>
	 * </ul>
	 * 
	 * <br>
	 * A CHECK_EDGE state is the first matching state on the stack when
	 * executing a MATCH_NAC_CALL, a CHECK_NAC_CALL or a NAC_TRANSLATION_CALL
	 * starting from the <a href="../../../../../doc/glossary.html">positive NAC
	 * interface</a> as these calls have predefined starting nodes from the
	 * current subgraph with corresponding counterparts from the host graph.
	 * 
	 * @param ms
	 *            the current matching state
	 */
	private void checkEdge(final MatchingState ms) {
		if (ms.backtrack == BackTrackReason.FAILURE) {
			if (this.matchingHistory != null && !this.matchingHistory.isEmpty()
					&& this.matchingHistory.getLast() != null && ms != this.matchingHistory.getLast()) {
				// where is the current ms in the history?
				final int index = this.matchingHistory.indexOf(ms);
				if (index > -1) {
					/*
					 * current matching state is not the latest state in the
					 * history, return all matchingStates coming after the
					 * current state from the history to the stack Stack has to
					 * be rebuilt, because the wrong matching is probably not on
					 * the stack, but in the history. So we have to check
					 * previous matchings because otherwise we might pop
					 * everything from the stack without finding the error.
					 */
					for (Iterator<MatchingState> msIter = this.matchingHistory.listIterator(index + 1); msIter
							.hasNext(); this.stack.push(msIter.next()))
						;
					if (stack.size() > 0) {
						stack.peek().backtrack = BackTrackReason.FAILURE;
					}
				}
			} else {
				// matchingState was the latest state in the history or there
				// was no history
				// find another edge that can be mapped to the current edge
				// next call should be checkEdge with the same matching state to
				// find another
				this.currentMatching.getEdgeMatching().remove(ms.currentEdge);
				this.matchingHistory.remove(ms);
			}
			ms.backtrack = BackTrackReason.NONE;
		} else if (ms.backtrack == BackTrackReason.BACKTRACK) {
			// we are in backtracking mode. This means we have to find a new
			// currentEdge for the current MatchingState to be matched
			// reset the iterator looking for unmatched edges
			ms.edgeIterator = null;
			final Edge nue = this.getNextUnmatchedEdge(ms);
			if (nue == null) {
				// no unmatched edge from the node in question, go back
				stack.pop();
				if (stack.size() > 0) {
					stack.peek().backtrack = BackTrackReason.BACKTRACK;
				}
			} else {
				// there is another edge, next call is checkEdge
				final MatchingState newMS = theFactory.getCheckEdgeState();
				newMS.currentEdge = nue;
				newMS.currentNode = ms.currentNode;
				newMS.mappedToNode = ms.mappedToNode;
				newMS.currentNAC = ms.currentNAC;
				newMS.mappedToNAC = ms.mappedToNAC;

				// NAC translation call
				if (mode == MatchMode.NAC_TRANSLATION_CALL) {
					newMS.edgeIterator = ms.edgeIterator;
				}

				stack.push(newMS);
			}
		} else {
			// default case, try to find a matching edge
			if (ms.currentEdge == null) {
				ms.currentEdge = this.getNextUnmatchedEdge(ms);

				if (ms.currentEdge == null) {
					// We did not find any unmatched edge, following we track
					// back to find further unmatched subgraph elements.
					stack.pop();
					if (stack.size() > 0) {
						// this is the only point where backtracking (not due to
						// failure) is activated
						// assuming we tried to match an edge that did not
						// exist, the next call is checkNode
						stack.peek().backtrack = BackTrackReason.BACKTRACK;
					}
					return;
				}
			}

			if (ms.mappedEdgeIterator == null) {
				ms.mappedEdgeIterator = iteratorOfEdges(ms.mappedToNode);
			}

			boolean foundMatch = findMatchingEdge(ms);

			if (foundMatch == false) {
				// we did not find a match for at least one Edge
				if (mode != MatchMode.NAC_TRANSLATION_CALL) {
					stack.pop();
					if (stack.size() > 0) {
						stack.peek().backtrack = BackTrackReason.FAILURE;
					}
				} else {
					/*
					 * When in NAC translation mode, we only search for
					 * incomplete matchings. So we can only "fail" when there
					 * are no unmatched edges left on a certain node in the
					 * current subgraph.
					 */
					Edge nue = getNextUnmatchedEdge(ms);
					if (nue == null) {
						stack.pop();
						if (stack.size() > 0) {
							stack.peek().backtrack = BackTrackReason.FAILURE;
						}
					} else {
						final MatchingState newMS = new MatchingState(MatchingOperation.CHECK_EDGE);
						newMS.currentEdge = nue;
						newMS.currentNode = ms.currentNode;
						newMS.mappedToNode = ms.mappedToNode;
						newMS.currentNAC = ms.currentNAC;
						newMS.mappedToNAC = ms.mappedToNAC;
						// nacTC
						if (mode == MatchMode.NAC_TRANSLATION_CALL) {
							newMS.edgeIterator = ms.edgeIterator;
						}
						stack.push(newMS);
					}
				}
			}
		}
	}

	/**
	 * This method finds an edge in the host graph for the current edge of the
	 * subgraph contained in the given matching state.
	 * 
	 * For an edge to be matched to the current edge, it must not be contained
	 * as a value in the current matching. Additionally, the predicates
	 * {@link #typePredicate(Edge, Edge), {@link #negatedPredicate(Edge, Edge)}}
	 * and {@link #directionPredicate(Edge, Edge, Node, Node)} need to be
	 * checked.<br>
	 * <br>
	 * If these conditions hold, the edges will be matched and added to the
	 * current matching. Depending on the nature of the edges, one of the
	 * following will happen:
	 * 
	 * <ul>
	 * <li>The edges are negated (i.e. belonging to NACs). A CHECK_NAC state
	 * will be put on the stack. This will result in the execution of the
	 * {@link #checkNAC()} method, which might result in the execution of a
	 * NAC_MATCH_CALL.</li>
	 * <li>The edges are positive and the node at the other end of the current
	 * edge is unmatched. A CHECK_NODE state with both nodes is put on the
	 * stack.</li>
	 * <li>The edges are positive and the node at the other end of the current
	 * edge has already been matched to the node at the other end of the mapped
	 * edge. This means that we do not need to match the nodes by creating a
	 * CHECK_NODE state. Instead, just search for unmatched edges going to or
	 * from the current node by putting a new CHECK_EDGE state on the stack.
	 * </li>
	 * </ul>
	 * <br>
	 * If no matching edge can be found, false will be returned. The calling
	 * method ({@link #checkNode(MatchingState)}) will handle this result.
	 * 
	 * @param ms
	 *            the current matching state
	 * @return true if there is a matching edge, false otherwise
	 */
	private boolean findMatchingEdge(final MatchingState ms) {
		final Iterator<Edge> theIterator = ms.mappedEdgeIterator;
		while (theIterator.hasNext()) {
			final Edge foundEdge = theIterator.next();
			// the blacklist condition is only used in NAC translation calls
			if (!currentMatching.getEdgeMatching().containsValue(foundEdge) && !blacklist.contains(foundEdge)) {
				// predicates
				if (typePredicate(ms.currentEdge, foundEdge) && negatedPredicate(ms.currentEdge, foundEdge)
						&& directionPredicate(ms.currentEdge, foundEdge, ms.currentNode, ms.mappedToNode)) {
					// get the nodes at the other side of the edge
					final Node newCurrentNode = ms.currentEdge.getSource() == ms.currentNode
							? ms.currentEdge.getTarget() : ms.currentEdge.getSource();
					final Node newFoundNode = foundEdge.getSource() == ms.mappedToNode ? foundEdge.getTarget()
							: foundEdge.getSource();

					if (!this.currentMatching.getNodeMatching().containsKey(newCurrentNode)) {
						// the nodes on the other side of the edge are unmatched
						this.currentMatching.getEdgeMatching().put(ms.currentEdge, foundEdge);
						this.matchingHistory.add(ms);

						final MatchingState newMS = theFactory.getCheckNodeState();
						newMS.currentNode = newCurrentNode;
						newMS.mappedToNode = newFoundNode;
						newMS.currentNAC = ms.currentNAC;
						newMS.mappedToNAC = ms.mappedToNAC;
						newMS.backtrack = BackTrackReason.NONE;

						// next call is check node
						stack.push(newMS);
						return true;
					} else if (this.currentMatching.getNodeMatching().get(newCurrentNode) == newFoundNode) {
						/*
						 * The nodes on the other side of the edge are already
						 * matched, so we found some kind of cycle. Therefore we
						 * will try to find another unmatched edge for the
						 * current matching state with its current node.
						 */
						this.currentMatching.getEdgeMatching().put(ms.currentEdge, foundEdge);
						this.matchingHistory.add(ms);
						if (this.mode == MatchMode.NAC_TRANSLATION_CALL) {
							this.iterativeMatchings.add(this.currentMatching.copy());
						}

						final MatchingState newMS = theFactory.getCheckEdgeState();
						newMS.currentNode = ms.currentNode;
						newMS.mappedToNode = ms.mappedToNode;
						newMS.currentNAC = ms.currentNAC;
						newMS.mappedToNAC = ms.mappedToNAC;

						// next call is check edge
						stack.push(newMS);
						return true;
					}
				} // if (type ...
			} // if (!currentMatching
		} // while...
		return false;
	}

	private void checkNAC() {
		MatchingState ms = stack.peek();
		if (ms.backtrack == BackTrackReason.FAILURE) {
			// remove nac matching
			currentMatching.getNacMatching().remove(ms.currentNAC);
			nacIterator = null;
			positiveFailure = true;
			stack.pop();
			if (stack.size() > 0) {
				stack.peek().backtrack = BackTrackReason.FAILURE;
			}
		} else if (ms.backtrack == BackTrackReason.BACKTRACK) {
			stack.pop();
			if (stack.size() > 0) {
				stack.peek().backtrack = BackTrackReason.BACKTRACK;
			}
		} else {

			// check whether bound items in NACs are part of the positive
			// matching so a translation is not necessary
			boolean translate = true;
			for (NegativeApplicationCondition nac : SamGraphInvCheckGraphAdapter.getInstance(hostGraph).getNacs()) {
				boolean allIn = true;
				if (nac.getAnnotations().isEmpty()) {
					allIn = false;
				}
				for (Annotation an : nac.getAnnotations()) {
					if (!currentMatching.getNodeMatching().containsValue(an.getTarget())
							&& !currentMatching.getEdgeMatching().containsValue(an.getTarget())) {
						allIn = false;
					}
				}
				if (allIn) {
					translate = false;
				}
			}
			// translate = true;
			NACTranslator nacT1 = new NACTranslator();
			nacT1.setMergedGraph((RuleGraph) hostGraph);
			nacT1.setInitialMatching(this.currentMatching.copy());
			nacT1.setPattern(pattern);
			if (nacT1.checkFullNacExistence()) {
				ms.backtrack = BackTrackReason.FAILURE;
				return;
			}
			// ms.translatedGraph = (RuleGraph) pattern;
			// if (ms.translatedGraph == null) {
			if (translate) {
				// if a translation is necessary, it should be done to the union
				// of the positive part of the pattern and the NAC interface in
				// the
				// host graph.
				NACTranslator nacT = new NACTranslator();
				// NACTranslatorOp nacT = new NACTranslatorOp();
				nacT.setMergedGraph((RuleGraph) hostGraph);
				nacT.setInitialMatching(this.currentMatching.copy());
				nacT.setPattern(pattern);
				if (nacT.checkFullNacExistence()) {
					ms.backtrack = BackTrackReason.FAILURE;
					return;
				}
				nacT.setInitialMatching(null);
				nacT.setMergedGraph(null);
				nacT.setPattern(null);
				// Match translation =
				// InvariantCheckingUtil.copyAsRuleGraph(hostGraph); // full
				// translation
				// translation to the minimum graph that includes the nac
				// interface and the pattern:
				Match translation = InvariantCheckerUtil.createMinimalTranslation(hostGraph, currentMatching);
				Graph translated = null;
				if (translation.getNodeMatching().size() > 0) {
					translated = (Graph) translation.getNodeMatching().get(0).getValue().eContainer();
				}
				if (translated == null && translation.getEdgeMatching().size() > 0) {
					translated = (Graph) translation.getEdgeMatching().get(0).getValue().eContainer();
				}

				// check whether host graph has necessary NACs to imply pattern
				// NACs, by type comparison
				/*
				 * Map<NodeType, Integer> nodeTypes = new HashMap<NodeType,
				 * Integer>(); for (NegativeApplicationCondition nac :
				 * SamGraphInvCheckGraphAdapter.getInstance(hostGraph).getNacs()
				 * ) { for (Node n : nac.getNodes()) { if
				 * (nodeTypes.containsKey(n.getInstanceOf())) {
				 * nodeTypes.put(n.getInstanceOf(),
				 * nodeTypes.get(n.getInstanceOf()) + 1); } else {
				 * nodeTypes.put(n.getInstanceOf(), 1); } } for (Annotation an :
				 * nac.getAnnotations()) { if
				 * (an.getSource().equals(InvariantCheckingCore.NAC_BOUND_ITEM))
				 * { if (SamgraphPackage.eINSTANCE.getNode().isSuperTypeOf(an.
				 * getTarget().eClass())) { Node n = (Node) an.getTarget(); if
				 * (nodeTypes.containsKey(n.getInstanceOf())) {
				 * nodeTypes.put(n.getInstanceOf(),
				 * nodeTypes.get(n.getInstanceOf()) + 1); } else {
				 * nodeTypes.put(n.getInstanceOf(), 1); } } } } // comparing one
				 * NAC should be enough break; } for (Map.Entry<NodeType,
				 * Integer> entry : nodeTypes.entrySet()) { boolean found =
				 * false; for (Node n : ms.currentNAC.getNodes()) { if
				 * (n.getInstanceOf() == entry.getKey()) { found = true; break;
				 * } } if (!found) { for (Node n : pattern.getNodes()) { if
				 * (!this.currentMatching.getNodeMatching().contains(n) &&
				 * translation.getNodeMatching().get(n) != null &&
				 * n.getInstanceOf() == entry.getKey()) { found = true; break; }
				 * } } if (!found) { ms.backtrack = BackTrackReason.FAILURE;
				 * return; } }
				 * 
				 */

				nacT.setMergedGraph((RuleGraph) translated);
				nacT.setPattern(pattern);
				Match initialMatching = SamtraceFactory.eINSTANCE.createMatch();
				for (Map.Entry<Node, Node> entry : currentMatching.getNodeMatching()) {
					initialMatching.getNodeMatching().put(entry.getKey(),
							translation.getNodeMatching().get(entry.getValue()));
				}
				for (Map.Entry<Edge, Edge> entry : currentMatching.getEdgeMatching()) {
					initialMatching.getEdgeMatching().put(entry.getKey(),
							translation.getEdgeMatching().get(entry.getValue()));
				}
				nacT.setInitialMatching(initialMatching);

				// print debug

				ms.translatedGraph = nacT.translateSingleNac(ms.currentNAC);
				if (ms.translatedGraph == null) {
					// positive occurrence of nac from current subgraph/pattern
					// in host graph
					// => abort, look for new positive matching
					ms.backtrack = BackTrackReason.FAILURE;
					return;
				}
				ms.translation = translation;
			} else {
				ms.translatedGraph = (RuleGraph) pattern;
			}
			GraphWithNacs tmp = SamGraphInvCheckGraphAdapter.getInstance(ms.translatedGraph);
			if (ms.currentNACIter == null) {
				ms.currentNACIter = tmp.getNacs().iterator(); // SamGraphInvCheckGraphAdapter.getInstance(ms.translatedGraph).getNacs().iterator();
			}
			if (ms.stack == null) {
				ms.stack = new Stack<NacMatchingState>();
			}
			if (ms.nacMatching == null) {
				ms.nacMatching = NacFactory.eINSTANCE.createMatchWithNacs();
			}

			while (ms.nacMatching.getNacMatching().size() < tmp.getNacs().size()) {
				if (ms.stack.size() > 0) {
					// System.out.println(ms.stack.peek());
					boolean triedAll = checkSingleNAC(ms);
					if (triedAll) {
						// tried all nacs from the host graph to fit in the nac
						// translated from
						// pattern to host.
						// now try to find forbidden graphs
						// (restrictingConstraints) in the nac (nac + pos.
						// elements)

						// boolean found = false;
						/*
						 * if (this.restrictingConstraints != null) {
						 * IsomorphicPartPartialMatcher subIpm = new
						 * IsomorphicPartPartialMatcher(); Match m =
						 * SubgraphIterator.fullNacToGraph(ms.stack.peek().
						 * currentNAC, true); Graph newHost = null; for (Node n
						 * : m.getNodeMatching().values()) { newHost = (Graph)
						 * n.eContainer(); break; }
						 * subIpm.setHostGraph(newHost);
						 * 
						 * for (Graph constraint : this.restrictingConstraints)
						 * { subIpm.setPattern(constraint);
						 * subIpm.setCurrentSubGraph(SubgraphIterator.
						 * graphToSubGraph(constraint)); subIpm.reset(); if
						 * (subIpm.getNextMatching() != null) { found = true;
						 * ms.nacMatching.getNacMatching().put(ms.stack.peek().
						 * currentNAC, null); break; } } } else {
						 */
						// this happens when there is no equivalent NAC in the
						// host graph for one (specific) NAC
						// in the translation of the current NAC to the host
						// graph
						ms.backtrack = BackTrackReason.FAILURE;
						// System.out.println("nac match failure");
						return;
						// }
					}
				} else {
					if (ms.currentNACIter.hasNext()) {
						NegativeApplicationCondition next = ms.currentNACIter.next();
						NacMatchingState newNMS = new NacMatchingState();
						newNMS.currentNAC = next;
						ms.stack.push(newNMS);
					}
				}
			}

			// add main nac matching
			currentMatching.getNacMatching().put(ms.currentNAC, ms.mappedToNAC);

			// successful matching: put next nac matching on the main stack
			if (nacIterator.hasNext()) {
				NegativeApplicationCondition next = nacIterator.next();
				MatchingState newMS = new MatchingState(MatchingOperation.CHECK_NAC);
				newMS.currentNAC = next;
				stack.push(newMS);

				// cleanup, trying to save some memory
				ms.nacMatching = null;
				ms.stack.clear();
				ms.translatedGraph = null;
				if (ms.translation != null) {
					ms.translation.clear();
				}
				ms.translation = null;
			}
		}
	}

	private boolean checkSingleNAC(MatchingState ms) {
		NacMatchingState nacms = ms.stack.peek();
		if (nacms.backtrack == BackTrackReason.FAILURE) {
			ms.stack.pop();
			if (ms.stack.size() > 0) {
				ms.stack.peek().backtrack = BackTrackReason.FAILURE;
			}
			return false;
		} else if (nacms.backtrack == BackTrackReason.BACKTRACK) {
			ms.stack.pop();
			if (ms.stack.size() > 0) {
				ms.stack.peek().backtrack = BackTrackReason.BACKTRACK;
			}
			return false;
		} else {
			if (nacms.mappedNACIter == null) {
				nacms.mappedNACIter = SamGraphInvCheckGraphAdapter.getInstance(hostGraph).getNacs().iterator();
			}
			if (nacms.mappedNACIter.hasNext()) {
				NegativeApplicationCondition mappedToNAC = nacms.mappedNACIter.next();
				// match successful: next nacmatchingstate, add to
				// currentMatching
				// match unsuccessful: leave on stack, try next turn other nac
				if (nacSizePredicate(nacms.currentNAC, mappedToNAC)
						&& nacInterfacePredicate(nacms.currentNAC, mappedToNAC)) {
					IsomorphicPartPartialMatcher subIPM = new IsomorphicPartPartialMatcher();
					// translate the current NAC (subgraph) to a positive
					// representation and save the mapping
					Match newHostNacMatch = SubgraphIterator.fullNacToGraph(nacms.currentNAC, false);
					// actually, the current NAC representation might be the
					// same if we just check another mappedNAC for the same
					// currentNAC.
					// so we could save the representation instead of
					// calculating it again to save some time.
					Graph newHost = null;
					for (Edge e : newHostNacMatch.getEdgeMatching().keySet()) {
						if (newHostNacMatch.getEdgeMatching().get(e) != null) {
							// this is the new (positive) graph representing the
							// NAC and its positive interface nodes
							newHost = (Graph) newHostNacMatch.getEdgeMatching().get(e).eContainer();
							break;
						}
					}
					if (newHost == null) {
						for (Node n : newHostNacMatch.getNodeMatching().keySet()) {
							if (newHostNacMatch.getNodeMatching().get(n) != null) {
								// this is the new (positive) graph representing
								// the NAC and its positive interface nodes
								newHost = (Graph) newHostNacMatch.getNodeMatching().get(n).eContainer();
								break;
							}
						}
					}

					// translate the "mapped" NAC (host graph) to a positive
					// representation and save the mapping
					Match newPatternNacMatch = SubgraphIterator.fullNacToGraph(mappedToNAC, true);
					Graph newPattern = null;
					for (Edge e : newPatternNacMatch.getEdgeMatching().keySet()) {
						if (newPatternNacMatch.getEdgeMatching().get(e) != null) {
							// this is the (positive) graph representing the NAC
							// and its positive interface nodes
							newPattern = (Graph) newPatternNacMatch.getEdgeMatching().get(e).eContainer();
							break;
						}
					}
					if (newPattern == null) {
						for (Node n : newPatternNacMatch.getNodeMatching().keySet()) {
							if (newPatternNacMatch.getNodeMatching().get(n) != null) {
								// this is the (positive) graph representing the
								// NAC and its positive interface nodes
								newPattern = (Graph) newPatternNacMatch.getNodeMatching().get(n).eContainer();
								break;
							}
						}
					}
					Set<AnnotatedElem> subgraph = SubgraphIterator.graphToSubGraph(newPattern);
					// the current NAC will be the current subgraph of the new
					// IPM instance
					subIPM.setCurrentSubGraph(subgraph);
					subIPM.setPattern(newPattern);
					// the "mapped" NAC will be the host graph of the new IPM
					// instance
					subIPM.setHostGraph(newHost);

					List<Node> interfaceBlacklist = new LinkedList<Node>();
					// build matching of the interface nodes
					Match interfaceMatching = SamtraceFactory.eINSTANCE.createMatch();
					// for (Map.Entry<Node, Node> entry :
					// currentMatching.getNodeMatching()) {
					// check whether this works
					for (Node n : hostGraph.getNodes()) {
						Node nodeInHostNac = null;
						Node nodeInPatternNac;
						if (ms.translation != null) {
							// Node nodeInTranslatedHost =
							// ms.translation.getNodeMatching().get(currentMatching.getNodeMatching().get(entry.getKey()));
							// // for translation
							Node nodeInTranslatedHost = ms.translation.getNodeMatching().get(n); // for
																									// translation
							// nodeInPatternNac =
							// newPatternNacMatch.getNodeMatching().get(currentMatching.getNodeMatching().get(entry.getKey()));
							// // for translation
							nodeInPatternNac = newPatternNacMatch.getNodeMatching().get(n); // for
																							// translation
							nodeInHostNac = newHostNacMatch.getNodeMatching().get(nodeInTranslatedHost); // for
																											// translation
						} else {
							for (Map.Entry<Node, Node> entry : currentMatching.getNodeMatching()) {
								if (entry.getValue() == n) {
									nodeInHostNac = newHostNacMatch.getNodeMatching().get(entry.getKey()); // only
																											// for
																											// non-translation
									break;
								}
							}
							// nodeInHostNac =
							// newHostNacMatch.getNodeMatching().get(entry.getKey());
							// // only for non-translation
							// nodeInHostNac =
							// newHostNacMatch.getNodeMatching().get(n); // only
							// for non-translation
							// nodeInPatternNac =
							// newPatternNacMatch.getNodeMatching().get(currentMatching.getNodeMatching().get(entry.getKey()));
							// // for non-translation
							nodeInPatternNac = newPatternNacMatch.getNodeMatching().get(n); // for
																							// non-translation
						}
						// Node nodeInHostNac =
						// newHostNacMatch.getNodeMatching().get(entry.getKey());
						// // only for non-translation
						// Node nodeInPatternNac =
						// newPatternNacMatch.getNodeMatching().get(currentMatching.getNodeMatching().get(entry.getKey()));
						// // for non-translation

						if (nodeInPatternNac != null && nodeInHostNac != null) {
							interfaceMatching.getNodeMatching().put(nodeInPatternNac, nodeInHostNac);
						} else if (nodeInPatternNac != null && nodeInHostNac == null) {
							// interfaces do not comply with positive matching,
							// try another nac
							return false;
						} else if (nodeInPatternNac == null && nodeInHostNac != null) {
							// this is the case where we can map a negative node
							// from a partial NAC to a positive node
							// from a total NAC. Consequently, we have an empty
							// blacklist.
							// interfaceBlacklist.add(nodeInHostNac);
						}
					}

					// initialize initial matching (positive interface nodes of
					// the NACs)
					// subIPM.handleNACMatchCall(ms.translation,
					// newPatternNacMatch, newHostNacMatch);
					subIPM.handleNACMatchCall(interfaceMatching, interfaceBlacklist);
					Match nacMatching = subIPM.getNextMatching();
					if (nacMatching != null) {
						// System.out.println("matched Nac");
						// found matching. If we just matched our "main" nac,
						// save the result.
						// not sure this works for partial NACs. Probably does
						// not matter.
						if (nacms.currentNAC.getNodes().size() == ms.currentNAC.getNodes().size()) {
							if (nacms.currentNAC.getEdges().size() == ms.currentNAC.getEdges().size()) {
								ms.mappedToNAC = mappedToNAC;
							}
						}

						// found matching, build next state on the stack
						if (ms.currentNACIter.hasNext()) {
							NegativeApplicationCondition next = ms.currentNACIter.next();
							NacMatchingState newNMS = new NacMatchingState();
							newNMS.currentNAC = next;
							ms.stack.push(newNMS);
						}
						// System.out.println("matched single nac");
						ms.nacMatching.getNacMatching().put(nacms.currentNAC, mappedToNAC);
						// todo: add matchings for nodes and edges.
						// Strictly speaking, this is unnecessary. For the
						// moment, at least.
						return false;
					} else {
						// no match: leave state on stack, try another nac next
						// turn
						return false;
					}
				} else {
					// predicates do not match; leave state on stack, try
					// another nac next turn
					return false;
				}
			} else {
				return true;
			}
		}
	}

	/**
	 * This comment is old, as the old checkNAC method does not exist any more.
	 * 
	 * This method handles a CHECK_NAC matching state. Such a state is
	 * initialized when {@link #findMatchingEdge(MatchingState)} matches two
	 * negative <a href="../../../../../doc/glossary.html">NAC interface
	 * edges</a> to each other. The NACs containing the edges will then be
	 * matched by a separate IPM instance executing a NAC_MATCH_CALL. It is
	 * important to note that such a state will only be created from within the
	 * {@link #findMatchingEdge(MatchingState)} method after handling a
	 * CHECK_EDGE state. Furthermore, CHECK_NAC states will only be created in
	 * MATCH_CALLs, but not in NAC_TRANSLATION_CALLs, CHECK_NAC_CALLs or
	 * NAC_MATCH_CALLs as these calls will work with positive elements only
	 * (some of which will represent negative items). <br>
	 * <br>
	 * The nature of the state might be:
	 * <dl>
	 * <dt>Failure</dt>
	 * <dd>Remove the state from the stack. Remove both NACs from the matching.
	 * Remove all items in the NACs from the matching. Set the previous state
	 * (will be a CHECK_EDGE state with two NAC interface edges) to FAILURE.
	 * </dd>
	 * <dt>Backtrack</dt>
	 * <dd>Remove the state from the stack. Set the previous state to BACKTRACK,
	 * continuing the backtracking process.</dd>
	 * <dt>None</dt>
	 * <dd>Try to match the NACs by executing a separate IPM instance with a
	 * NAC_MATCH_CALL. To prepare this call, the following steps will be
	 * executed:</dd>
	 * </dl>
	 * <ol>
	 * <li>Check the
	 * {@link #nacSizePredicate(NegativeApplicationCondition, NegativeApplicationCondition)}
	 * , the
	 * {@link #nacInterfacePredicate(NegativeApplicationCondition, NegativeApplicationCondition)}
	 * and the {@link #mappedNacInterface(NegativeApplicationCondition)}
	 * predicate. If any of these conditions do not hold, remove the state from
	 * the stack and set the previous state to FAILURE.</li>
	 * <li>Create a new IPM instance. Create a
	 * <a href="../../../../../doc/glossary.html">positive representation</a>
	 * for the current NAC (from the current subgraph) and set it as the new
	 * IPM's current subgraph and pattern.</li>
	 * <li>Create a positive representation for the mapped NAC (from the host
	 * graph) and set it as the new IPM's host graph.</li>
	 * <li>Call
	 * {@link #handleNACMatchCall(NegativeApplicationCondition, Match, Match, Match)}
	 * , passing the current NAC, the match mapping it to its positive
	 * representation, the match mapping the mapped NAC to its positive
	 * representation and the current matching. This method will translate the
	 * current matching to the new subgraph and host graph so that the
	 * NAC_MATCH_CALL will have the positive NAC interface as starting points
	 * which will already be matched.</li>
	 * <li>Execute the new IPM instance by calling {@link #getNextMatching()}.
	 * </li>
	 * <li>If there is a result, call
	 * {@link #completeNACMatching(MatchingState, NegativeApplicationCondition, NegativeApplicationCondition)}
	 * . This method will issue a CHECK_NAC_CALL in another IPM instance, which
	 * will ensure that the NAC does not illegally exist as a positive part of
	 * the unmatched host graph. It it does exist or if the result of the
	 * NAC_MATCH_CALL is null, the NACs can not be matched. In that case remove
	 * the state from the stack and set the previous state (will be the
	 * CHECK_EDGE state containing two NAC interface edges) to FAILURE.</li>
	 * <li>Add the two NACs to the current matching.</li>
	 * <li>The matching returned by the NAC_MATCH_CALL matches only the positive
	 * representations of the NACs to each other. Therefore we need to translate
	 * the matching to our original NACs in the current subgraph and host graph.
	 * </li>
	 * <li>Add the matching of the graph items in the NACs to the current
	 * matching. If a CHECK_NAC state with FAILURE is handled, all the items
	 * will be removed from the current matching. So basically, the matching of
	 * the graph items is tied to the CHECK_NAC state.
	 * <li>Create a new CHECK_EDGE state and put it on the stack. The nodes will
	 * be the same as the nodes of the CHECK_EDGE stack that originally lead to
	 * the matching of two negative edges and to this CHECK_NAC call. These
	 * nodes will usually be part of the
	 * <a href="../../../../../doc/glossary.html">positive NAC interface</a> As
	 * the NAC items were matched by the NAC_MATCH_CALL, the matching process
	 * will continue with the positive part of the current subgraph.</li>
	 * </ol>
	 * 
	 */

	/**
	 * This predicate checks whether the interfaces of two NACs contain the same
	 * types, which is a necessary requirement for the NACs to be matched.
	 * 
	 * @param currentNAC
	 *            the current NAC
	 * @param mappedToNAC
	 *            the "mapped" NAC
	 * @return true if the the interfaces contain the same number of items for
	 *         every type, false otherwise
	 */
	private boolean nacInterfacePredicate(NegativeApplicationCondition currentNAC,
			NegativeApplicationCondition mappedToNAC) {
		if (true) {
			return true;
		}
		HashMap<EdgeType, Integer> typeMapC = new HashMap<EdgeType, Integer>();
		HashMap<EdgeType, Integer> typeMapM = new HashMap<EdgeType, Integer>();
		for (Edge e1 : currentNAC.getEdges()) {
			if (e1.partOfNacInterface()) {
				if (typeMapC.containsKey(e1.getInstanceOf())) {
					typeMapC.put(e1.getInstanceOf(), typeMapC.get(e1.getInstanceOf()) + 1);
				} else {
					typeMapC.put(e1.getInstanceOf(), 1);
				}
			}
		}
		for (Edge e1 : mappedToNAC.getEdges()) {
			if (e1.partOfNacInterface()) {
				if (typeMapM.containsKey(e1.getInstanceOf())) {
					typeMapM.put(e1.getInstanceOf(), typeMapM.get(e1.getInstanceOf()) + 1);
				} else {
					typeMapM.put(e1.getInstanceOf(), 1);
				}
			}
		}
		for (EdgeType s : typeMapM.keySet()) {
			if (!typeMapC.containsKey(s)) {
				return false;
			} else if (typeMapM.get(s) > typeMapC.get(s)) {
				return false;
			}
		}
		return true;
	}

	/**
	 * This predicate compares the sizes of the NAC, ensuring a necessary
	 * requirement for the NACs to be matched.
	 * 
	 * @param currentNAC
	 *            the current NAC
	 * @param mappedToNAC
	 *            the "mapped" NAC
	 * @return false if the current NAC is smaller than the "mapped" NAC, true
	 *         otherwise
	 */
	private boolean nacSizePredicate(NegativeApplicationCondition currentNAC,
			NegativeApplicationCondition mappedToNAC) {
		if (currentNAC.getNodes().size() < mappedToNAC.getNodes().size()) {
			// return false;
		}
		return true;
	}

	/**
	 * Compare the types of two edges.
	 * 
	 * @param e1
	 *            one edge
	 * @param e2
	 *            another edge
	 * @return true if the edges have the same type, false otherwise
	 */
	private boolean typePredicate(final Edge e1, final Edge e2) {
		if (e1 != null && e2 != null) {
			return (e1.getInstanceOf() == null || e2.getInstanceOf() == null
					|| e1.getInstanceOf().equals(e2.getInstanceOf()));
		} else if (e1 == e2) {
			return true;
		}
		return false;
	}

	/**
	 * Compare the types of two nodes.
	 * 
	 * @param n1
	 *            one node
	 * @param n2
	 *            another node
	 * @return true if the nodes have the same type, false otherwise
	 */
	private boolean typePredicate(final Node n1, final Node n2) {
		if (n1 != null && n2 != null) {
			return n1.getInstanceOf() == null || n2.getInstanceOf() == null
					|| n1.getInstanceOf().equals(n2.getInstanceOf());
		} else if (n1 == n2) {
			return true;
		}
		return false;
	}

	/**
	 * Compare the direction of two edges.
	 * 
	 * @param e1
	 *            one edge
	 * @param e2
	 *            another edge
	 * @param n1
	 *            a node adjacent to e1 (source or target)
	 * @param n2
	 *            a node adjacent to e2 (source or target)
	 * @return true if the edges have the same direction, false otherwise
	 */
	private boolean directionPredicate(final Edge e1, final Edge e2, final Node n1, final Node n2) {
		if (e1 != null && e2 != null) {
			return e1.getInstanceOf().getDirection() == e2.getInstanceOf().getDirection()
					&& (e1.getInstanceOf().getDirection() == EdgeDirection.UNDIRECTED
							|| ((e1.getSource() == n1 && e2.getSource() == n2)
									|| (e1.getTarget() == n1 && e2.getTarget() == n2)));
		} else if (e1 == e2) {
			return true;
		}
		return false;
	}

	/**
	 * Check whether the edges are both negative or both positive.
	 * 
	 * @param e1
	 *            one edge
	 * @param e2
	 *            another edge
	 * @return true if both edges are negative or positive, false otherwise
	 */
	private boolean negatedPredicate(final Edge e1, final Edge e2) {
		if (e1 != null && e2 != null) {
			return (InvariantCheckerUtil.isNegated(e1) == InvariantCheckerUtil.isNegated(e2));
		} else if (e1 == e2) {
			return true;
		}

		return false;
	}

	/**
	 * Check whether the nodes are both negative or both positive.
	 * 
	 * @param n1
	 *            a node
	 * @param n2
	 *            another node
	 * @return true if both nodes are negative or positive, false otherwise
	 */
	private boolean negatedPredicate(final Node n1, final Node n2) {
		if (mode == MatchMode.NAC_TRANSLATION_CALL) {
			return true;
		}
		if (n1 != null && n2 != null) {
			return InvariantCheckerUtil.isNegated(n1) == InvariantCheckerUtil.isNegated(n2);
		} else if (n1 == n2) {
			return true;
		}

		return false;
	}

	/**
	 * This method builds all incomplete matchings of the given graphs. It is
	 * used by the NACTranslator component. It is executed in the context of a
	 * NAC_TRANSLATION_CALL. If the subgraph can be found in the host graph,
	 * null is returned.
	 * 
	 * @return a list of matchings or null, if a complete matching can be found
	 */
	public LinkedList<Match> getIterativeMatchings() {
		if (this.getNextMatching() != null) {
			return null;
		} else {
			LinkedList<Match> result = new LinkedList<Match>();
			for (Match gm : iterativeMatchings) {
				result.add(gm.copy());
			}
			return result;
		}
	}

	private boolean nacInterfaceNodePredicate(Node expected, Node found) {
		if (mode == MatchMode.NAC_MATCH_CALL) {
			if (this.nacInterfaceMatch.getNodeMatching().containsKey(expected)) {
				return this.nacInterfaceMatch.getNodeMatching().get(expected) == found;
			} else {
				// the first part of the condition is probably obsolete
				return !this.nacInterfaceMatch.getNodeMatching().containsValue(found) && !nodeBlacklist.contains(found);
			}
		} else if (mode == MatchMode.NAC_TRANSLATION_CALL) {
			if (this.nacInterfaceMatch.getNodeMatching().containsKey(expected)) {
				return this.nacInterfaceMatch.getNodeMatching().get(expected) == found;
			} else {
				return !this.nodeBlacklist.contains(found);
			}
		} else {
			return true;
		}
	}

	/**
	 * This predicate returns true if the degree of the first node is greater or
	 * equal the second node's degree.<br />
	 * A node's degree is specified as the sum of the numbers of its in- and
	 * outgoing edges.
	 * 
	 * @param n1
	 *            the first node
	 * @param n2
	 *            the second node
	 * @return true if the first node's degree is greater or equal the second
	 *         node's degree.
	 */
	private boolean degreePredicate(final Node n1, final Node n2) {
		if (n1 != null && n2 != null) {
			// addition to negative nodes
			if (mode == MatchMode.NAC_TRANSLATION_CALL || mode == MatchMode.NAC_MATCH_CALL) {
				return true;
			}
			if (InvariantCheckerUtil.isNegated(n1) && InvariantCheckerUtil.isNegated(n2)) {
				return true;
			}
			if (this.nodeDegrees == null || !this.nodeDegrees.containsKey(n2)) {
				return false;
			}
			final int degree = this.nodeDegrees.get(n2);
			return (n1.getIncoming().size() + n1.getOutgoing().size()) >= degree;
		}
		return false;
	}

	/**
	 * This method returns a <code>Vector</code> containing all matchings
	 * between the currently set
	 * {@link IsomorphicPartPartialMatcher#setCurrentSubGraph(Set) subgraph} and
	 * the set property attribute of this object. Note, that you have to invoke
	 * this method for each subgraph of a rule Graph to compute all partial
	 * matchings between rule and property.
	 *
	 * @return a <code>{@link Vector Vector}</code> containing all matchings
	 *         between the property and the rule restricted to the current
	 *         subgraph of this object.
	 * @see IsomorphicPartPartialMatcher#setCurrentSubGraph(Set)
	 * @see IsomorphicPartPartialMatcher#setHostGraph(Graph)
	 * @see IsomorphicPartPartialMatcher#setPattern(Graph)
	 * @see org.eclipse.emf.henshin.sam.invcheck.SubgraphIterator
	 */
	public Vector<Match> findAllMatchings() {
		Vector<Match> results = new Vector<Match>();
		if (this.currentSubGraph != null && this.pattern != null && this.hostGraph != null) {
			this.reset();
			Match gm = this.getNextMatching();
			while (gm != null) {
				results.add(gm);
				gm = this.getNextMatching();
			}
		}
		return results;
	}

	/**
	 * Get the currentSubGraph attribute of the IsomorphicPartMatcher object
	 *
	 * @return The currentSubGraph value
	 */
	public Set<AnnotatedElem> getCurrentSubGraph() {
		return currentSubGraph;
	}

	/**
	 * Sets the currentSubGraph attribute of the IsomorphicPartMatcher object.
	 * <br />
	 * Changing an <code>IsomorphicPartMatcher</code>'s subgraph attribute,
	 * invalidates the <code>IsomorphicPartMatcher</code>'s internal state. You
	 * have to invoke {@link #reset()} prior to invoking
	 * {@link #getNextMatching()} to receive valid matches.
	 *
	 * @param subGraph
	 *            The new currentSubGraph value
	 */
	public void setCurrentSubGraph(Set<AnnotatedElem> subGraph) {
		if (this.currentSubGraph != subGraph) {
			this.currentSubGraph = subGraph;
		}

	}

	/**
	 * Builds an iterator for all nodes coming from or going to the given node.
	 * 
	 * @param n
	 *            a node
	 * @return an iterator of edges
	 */
	private Iterator<Edge> iteratorOfEdges(Node n) {
		EList<Edge> all = new BasicEList<Edge>();
		for (Edge e : n.getIncoming()) {
			all.add(e);
		}
		for (Edge e : n.getOutgoing()) {
			if ((e.getSource() == e.getTarget()) == false)
				all.add(e);
		}
		return all.iterator();
	}

	/**
	 * In a first step this method computes a <code>Map</code> that contains the
	 * frequency of types in the <code>Set</code> s. Afterwards each entry in
	 * this <code>Map</code> gets compared to the corresponding value of the
	 * given <code>Graph</code>. Contains the <code>Set</code> more elements of
	 * a type then the <code>Graph</code> the method returns false. In this case
	 * there is no need to compute all matchings, as none exists.
	 *
	 * @param s
	 * @param g
	 * @return
	 */
	private boolean compareTypes(Set<AnnotatedElem> s, Graph g) {
		// compute types in host graph

		if (s != null && g != null) {
			Map<NodeType, Integer> m = SubgraphIterator.computeTypesInSubgraph(s);
			for (Iterator<Map.Entry<NodeType, Integer>> iter = m.entrySet().iterator(); iter.hasNext();) {
				Map.Entry<NodeType, Integer> entry = iter.next();
				Integer i = entry.getValue();
				// if (i.intValue() > g.getNumberOfType(entry.getKey())) {
				if (i.intValue() > 0 && !this.typeCount.containsKey(entry.getKey())) {
					return false;
				} else if (i.intValue() > this.typeCount.get(entry.getKey())) {
					return false;
				}
			}
			return true;
		}
		return false;
	}

	public enum MatchMode {
		MATCH_CALL, NAC_MATCH_CALL, NAC_TRANSLATION_CALL;
	}

	public static class NacMatchingState {
		public NegativeApplicationCondition currentNAC;
		public Iterator<NegativeApplicationCondition> mappedNACIter;
		BackTrackReason backtrack;

		public NacMatchingState() {

		}

		@Override
		public String toString() {
			StringBuffer sb = new StringBuffer(20);
			sb.append("Single NAC matching");
			sb.append(": ");
			sb.append(this.currentNAC.getNodes().size());
			return sb.toString();
		}

	}

	public static class MatchingState {
		public Node currentNode;
		public Node mappedToNode;
		public Iterator<Edge> edgeIterator;
		public Iterator<Edge> mappedEdgeIterator;
		public Edge currentEdge;
		public NegativeApplicationCondition currentNAC;
		public NegativeApplicationCondition mappedToNAC;
		public RuleGraph translatedGraph; // only for nac matching
		public Iterator<NegativeApplicationCondition> currentNACIter; // only
																		// for
																		// nac
																		// matching
		public MatchWithNacs nacMatching; // only for nac matching
		public Stack<NacMatchingState> stack; // only for nac matching
		public Match translation; // only for nac matching
		BackTrackReason backtrack;
		final MatchingOperation matchOp;

		public MatchingState(MatchingOperation mo) {
			this.matchOp = mo;
		}

		enum MatchingOperation {
			CHECK_EDGE, CHECK_NODE, CHECK_NAC;
		}

		enum BackTrackReason {
			NONE, FAILURE, BACKTRACK;
		}

		@Override
		public String toString() {
			StringBuffer sb = new StringBuffer(20);
			sb.append(this.matchOp);
			sb.append(" ").append(this.currentNode != null ? this.currentNode.getName() : "null");
			sb.append("->").append(this.mappedToNode != null ? this.mappedToNode.getName() : "null");
			if (matchOp == MatchingOperation.CHECK_EDGE) {
				sb.append(this.currentEdge != null ? this.currentEdge : "null");
			}
			if (matchOp == MatchingOperation.CHECK_NAC) {
				/*
				 * for (Edge e : this.currentNAC.getEdges()) { sb.append(e);
				 * sb.append(","); } sb.append("--"); for (Edge e :
				 * this.mappedToNAC.getEdges()) { sb.append(e); sb.append(",");
				 * }
				 */
			}
			return sb.toString();
		}
	}

	public class TestAdapter {

		public class TestAdapterMatchingStateFactory extends MatchingStateFactory {
			TestAdapterMatchingStateFactory(final int a, final int b) {
				super(a, b);
			}
		};

		public void setStartNode(Node n) {
			connectedComponents.get(0).startNode = n;
		}

		public void pushCheckNodeMatchingState(Node current, Node mappedTo) {
			if (stack != null) {
				MatchingState ms = new MatchingState(MatchingOperation.CHECK_NODE);
				ms.currentNode = current;
				ms.mappedToNode = mappedTo;
				stack.push(ms);
			}
		}

		public void setHostNodeIter(Iterator<Node> iter) {
			connectedComponents.get(0).hostNodeIter = iter;
		}

		public boolean testTypePredicate(Edge e1, Edge e2) {
			return typePredicate(e1, e2);
		}

		public boolean testDirectionPredicate(Edge e1, Edge e2, Node n1, Node n2) {
			return directionPredicate(e1, e2, n1, n2);
		}

		public boolean testNegatedPredicate(Edge e1, Edge e2) {
			return negatedPredicate(e1, e2);
		}

		public TestAdapterMatchingStateFactory getFactory() {
			return new TestAdapterMatchingStateFactory(5, 5);
		}
	}
}

/*
 * $Log$ Revision 1.4 2007/06/25 17:48:22 basilb fixed a lot of these bugs
 * testing does not find but evaluating ;)
 *
 * Revision 1.3 2007/01/11 14:44:23 basilb even more usage of generics
 *
 * Revision 1.2 2007/01/03 09:27:46 basilb removed compile errors caused by
 * wrong import declarations; introduced empty plugin class to ensure correct
 * loading
 *
 */