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

/**
 * Depth first search.
 * 
 * @author Franck van Breugel
 */
public class DFSearch extends Search {
	public DFSearch(Config config, VM vm) {
		super(config, vm);
	}

	protected boolean forward() {
		boolean successful = super.forward();
		if (successful) {
			this.notifyStateAdvanced();
			this.depth++;
			if (this.getCurrentError() != null) {
				this.notifyPropertyViolated();
			}
		} else {
			this.notifyStateProcessed();
		}
		return successful;
	}

	protected boolean backtrack() {
		boolean successful = super.backtrack();
		if (successful) {
			this.notifyStateBacktracked();
			this.depth--;
		}
		return successful;
	}

	public boolean checkStateSpaceLimit() {
		boolean available = super.checkStateSpaceLimit();
		if (!available) {
			this.notifySearchConstraintHit("memory limit reached: " + this.minFreeMemory);
		}
		return available;
	}

	private boolean checkDepthLimit() {
		boolean below = this.depth < this.getDepthLimit();
		if (!below) {
			this.notifySearchConstraintHit("depth limit reached: " + this.depth);
		}
		return below;
	}

	public void search() {
		this.notifySearchStarted();
		do {
			while (!this.done &&
					!this.checkAndResetBacktrackRequest() &&
					this.forward() &&
					this.isNewState() &&
					!this.isEndState() &&
					!this.isIgnoredState() &&
					this.checkDepthLimit() &&
					this.checkStateSpaceLimit()) {
				// do nothing
			}
		} while (!this.done &&
				this.backtrack() &&
				this.checkStateSpaceLimit());
		this.notifySearchFinished();
	}
}