package search; 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; /** * Breadth first search. * * @author Franck van Breugel */ public class BFSearch extends Search { /** * Initializes this search. * * @param config JPF's configuration * @param vm JPF's VM */ public BFSearch(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(); 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(); } 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.done = true; 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; } /** * 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); } /** * Checks whether this search support backtrack requests. * It does not. * * @return false */ public boolean supportBacktrack() { return false; } /** * Searches the state space. */ @Override public void search() { this.notifySearchStarted(); Queue queue = new LinkedList(); queue.offer(this.getRestorableState()); this.notifyStateStored(); queue.offer(null); while (!this.done && queue.size() > 1 && this.checkDepthLimit()) { RestorableVMState state = queue.poll(); if (state == null) { this.depth++; queue.offer(null); } else { this.restoreState(state); this.notifyStateRestored(); while (!this.done && this.forward() && this.checkStateSpaceLimit() && !this.hasPropertyTermination()) { if (!this.isErrorState() && this.isNewState() && !this.isEndState() && !this.isIgnoredState()) { queue.offer(this.getRestorableState()); this.notifyStateStored(); } this.backtrack(); } } } this.notifySearchFinished(); } }