import java.util.LinkedList;
import java.util.Queue;

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

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

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

	/**
	 * Drives the search.
	 */
	@Override
	public void search() {
		this.notifySearchStarted();
		Queue<RestorableVMState> queue = new LinkedList<RestorableVMState>();
		queue.offer(this.getRestorableState());
		queue.offer(null);
		while (!queue.isEmpty() && !this.done && this.checkDepthLimit() && this.checkStateSpaceLimit()) {
			RestorableVMState state = queue.poll();
			if (state == null) {
				this.depth++;
				queue.offer(null);
			} else {
				this.restoreState(state);
				while (this.forward() && !this.done && this.checkStateSpaceLimit()) {
					if (this.isNewState() && !this.isIgnoredState()) {
						queue.offer(this.getRestorableState());
						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 this search strategy support requests for backtracks.
	 * 
	 * @return true if this search strategy support requests for backtracks,
	 * false otherwise.
	 */
	public boolean supportBacktrack() {
		return false;
	}

	/**
	 * Returns the current state so that it is restorable.
	 * 
	 * @return the current state.
	 */
	private RestorableVMState getRestorableState() {
		return this.getVM().getRestorableState();
	}
	/**
	 * Restores the given state.
	 * 
	 * @param state a state that is restorable.
	 */
	private void restoreState(RestorableVMState state) {
		this.getVM().restoreState(state);
	}

	/**
	 * 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;
	}
}