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

/**
 * This class implements the depth first search strategy.
 * 
 * @author Franck van Breugel
 */
public class DFSearch extends Search {

	/**
	 * Initializes this search strategy.
	 * 
	 * @param config JPF's configuration.
	 * @param vm JPF's virtual machine.
	 */
	public DFSearch(Config config, VM vm) {
		super(config, vm);
	}

	/**
	 * Drives the search.
	 */
	@Override
	public void search() {
		this.notifySearchStarted();
		this.depth = 1;
		do {
			this.depth--;
			while (!this.isIgnoredState() && 
					!this.done &&
					!this.checkAndResetBacktrackRequest() && 
					this.checkDepthLimit() &&
					this.checkStateSpaceLimit() &&
					this.forward() &&
					!this.hasPropertyTermination()) {
				this.depth++;
			}
		} while (!this.done && 
				this.checkStateSpaceLimit() &&
				this.backtrack());
		this.notifySearchFinished();
	}

	/**
	 * Attempts to traverse an unexplored transition.  If successful,
	 * notifies all listeners that JPF advanced to the next state.
	 * If not successful, notifies all listeners that JPF processed
	 * the current state.  If successful and a violation of a property
	 * was detected while traversing the transition, notifies all
	 * listeners that JPF detected a property violation.
	 * 
	 * @return true if there is an unexplored transition, false otherwise.
	 */
	@Override
	protected boolean forward() {
		boolean successful = super.forward();
		if (successful) {
			this.notifyStateAdvanced();
			if (this.getCurrentError() != null) {
				this.notifyPropertyViolated();
			}
		} else {
			this.notifyStateProcessed();
		}
		return successful;
	}

	/**
	 * Attempts to backtrack.  If successful, notifies all listeners that 
	 * JPF backtracked. 
	 * 
	 * @return true if the backtrack is successful, false otherwise.
	 */
	@Override
	protected boolean backtrack() {
		boolean successful = super.backtrack();
		if (successful) {
			this.notifyStateBacktracked();
		}
		return successful;
	}

	/**
	 * Tests whether there is a minimum amount of free memory left. 
	 * If no such minimum amount of free memory is left, notifies all 
	 * listeners that JPF has reached its memory limit.
	 * 
	 * At this point, it is advised to stop this search (with a threshold 
	 * amount left) so that something useful can be reported, instead of 
	 * dying silently with an OutOfMemoryError.
	 * 
	 * @return true if there is a minimum amount of free memory left,
	 * false otherwise.
	 */
	@Override
	public boolean checkStateSpaceLimit() {
		boolean available = super.checkStateSpaceLimit();
		if (!available) {
			this.notifySearchConstraintHit("memory limit reached");
		} 
		return available;
	}

	/**
	 * Tests whether the depth is smaller than the depth limit.
	 * If this is not the case, notifies all listeners that JPF 
	 * has reached its depth limit.
	 * 
	 * @return true if the depth is smaller than the depth limit,
	 * false otherwise.
	 */
	private boolean checkDepthLimit() {
		boolean below = this.depth < this.getDepthLimit();
		if (!below) {
			this.notifySearchConstraintHit("depth limit reached");
		}
		return below;
	}
}