import gov.nasa.jpf.Config;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.vm.VM;

public class DFSearch extends Search {
	public DFSearch(Config config, VM vm) {
		super(config, vm);
	}
	
	public void search() {
		final int MAX_DEPTH = getDepthLimit();
		int depth = 0;
		notifySearchStarted();
		while (!done && checkStateSpaceLimit()) {
			if (isEndState() || isIgnoredState() || checkAndResetBacktrackRequest() || depth >= MAX_DEPTH || !forward()) {
				if (!backtrack()) {
					break;
				} else {
					notifyStateBacktracked();
					depth--;
				}
			} else {
				if (hasPropertyTermination()) {
					break;
				}
				notifyStateAdvanced();
				depth++;
			}
		}
		notifySearchFinished();
	}
}