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

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

public class BFSearch extends Search {
	public BFSearch(Config config, VM vm)
	{
		super(config, vm);
	}

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

	protected boolean backtrack() {
		boolean successful = super.backtrack();
		if (successful) {
			this.notifyStateBacktracked();
		}
		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;
	}

	private RestorableVMState getRestorableState() {
		return this.getVM().getRestorableState();
	}

	private void restoreState(RestorableVMState state) {
		this.getVM().restoreState(state);
	}

	public void search() {
		this.notifySearchStarted();
		Queue<RestorableVMState> queue = new LinkedList<RestorableVMState>();
		queue.offer(this.getRestorableState());
		this.notifyStateStored();
		queue.offer(null);
		this.depth = 1;
		while (!this.done && queue.size() > 1) {
			RestorableVMState state = queue.poll();
			if (state == null) {
				this.depth++;
				queue.offer(null);
			} else {
				this.restoreState(state);
				this.notifyStateRestored();
				while (!this.done && this.forward()) {
					if (!this.checkStateSpaceLimit() || this.hasPropertyTermination()) {
						this.done = true;
					} else {
						if (this.isNewState() && !this.isEndState() && !this.isIgnoredState() && this.checkDepthLimit()) {
							queue.offer(this.getRestorableState());
							this.notifyStateStored();
						}
						this.backtrack();
					}
				}
			}
		}
		this.notifySearchFinished();
	}

	public boolean supportBacktrack() {
		return false;
	}
}