package search;

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 {
	
	/**
	 * Initializes this search.
	 * 
	 * @param config JPF's configuration
	 * @param vm JPF's VM
	 */
	public DFSearch(Config config, VM vm) {
		super(config, vm);
	}

	/**
	 * Attempts to traverse an unexplored transition.  If 
	 * successful, notifies that this search advanced to another 
	 * state.  If successful and a property was violated by 
	 * the traversed transition, then notifies this.  If not 
	 * successful, notifies that the current state has been
	 * fully explored. 
	 * 
	 * @return true if this search traverses a transition,
	 * false otherwise
	 */
	@Override
	protected boolean forward() {
		boolean successful = super.forward();
		if (successful) {
			this.notifyStateAdvanced();
			this.depth++;
			if (this.getCurrentError() != null) {
				this.notifyPropertyViolated();
			}
		} else {
			this.notifyStateProcessed();
		}
		return successful;
	}

	/**
	 * Attempts to backtrack.  If successful, notifies that
	 * this search backtracked to the previous state.
	 * 
	 * @return true if this search backtracked, false otherwise
	 */
	@Override
	protected boolean backtrack() {
		boolean successful = super.backtrack();
		if (successful) {
			this.notifyStateBacktracked();
			this.depth--;
		}
		return successful;
	}

	/**
	 * Checks whether the memory limit has been reached.  If it has,
	 * then notifies this.
	 * 
	 * @return true if the memory limit has not been reached,
	 * false otherwise
	 */
	@Override
	public boolean checkStateSpaceLimit() {
		boolean available = super.checkStateSpaceLimit();
		if (!available) {
			this.notifySearchConstraintHit("memory limit reached: " + this.minFreeMemory);
		}
		return available;
	}

	/**
	 * Checks whether the depth limit has been reached.  If it has,
	 * then notifies this.
	 * 
	 * @return true if the depth limit has not been reached,
	 * false otherwise
	 */
	private boolean checkDepthLimit() {
		boolean below = this.depth < this.getDepthLimit();
		if (!below) {
			this.notifySearchConstraintHit("depth limit reached: " + this.depth);
		}
		return below;
	}

	/**
	 * Searches the state space.
	 */
	@Override
	public void search() {
		this.notifySearchStarted();
		do {
			while (!this.done &&
					!this.checkAndResetBacktrackRequest() &&
					this.forward() &&
					this.checkDepthLimit() &&
					this.isNewState() &&
					!this.isEndState() &&
					!this.isIgnoredState() &&
					this.checkStateSpaceLimit() &&
					!this.hasPropertyTermination()) {
				// do nothing
			}
		} while (!this.done &&
				this.backtrack() &&
				this.checkStateSpaceLimit());
		this.notifySearchFinished();
	}
}