import java.util.LinkedList;
import java.util.List;

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);
	}

	@Override
	public void search() {
		notifySearchStarted();
		final int MAX_DEPTH = getDepthLimit();
		depth = 0;
		List<RestorableVMState> currentLevel = new LinkedList<RestorableVMState>();
		currentLevel.add(vm.getRestorableState());
		notifyStateStored();
		while (!currentLevel.isEmpty() && !done && depth < MAX_DEPTH) {
			List<RestorableVMState> nextLevel = new LinkedList<RestorableVMState>();
			for (RestorableVMState state : currentLevel) {
				vm.restoreState(state);
				notifyStateRestored();
				while (forward() && !done) {
					notifyStateAdvanced();
					if (currentError != null) {
						notifyPropertyViolated();
					}
					if (!checkStateSpaceLimit()) {
						notifySearchConstraintHit("memory limit reached");
						done = true;
					} else if (hasPropertyTermination()) {
						done = true;
					} else if (isNewState() && !isEndState() && !isIgnoredState()) {
						nextLevel.add(vm.getRestorableState());
						notifyStateStored();
					}
					notifyStateProcessed();
					backtrack();
					notifyStateBacktracked();
				}
			}
			currentLevel = nextLevel;
			depth++;
			if (depth >= MAX_DEPTH) {
				notifySearchConstraintHit("depth limit reached");
				done = true;
			}
		}
		notifySearchFinished();
	}

	public boolean supportBacktrack() {
		return false;
	}

}