--- /dev/null
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package gov.nasa.jpf.search.heuristic;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.search.Search;
+import gov.nasa.jpf.vm.VM;
+
+import java.util.ArrayList;
+import java.util.List;
+
+
+/**
+ * a search strategy class that computes all immediate successors of a given
+ * state, puts them into a priority queue (the priority is provided by a
+ * Heuristic strategy object), and processes states in the sequence of
+ * highest priorities. Note that the queue can be search-global, i.e. we might hop
+ * between search levels.
+ */
+public abstract class HeuristicSearch extends Search {
+
+ static final String DEFAULT_HEURISTIC_PACKAGE = "gov.nasa.jpf.search.heuristic.";
+
+ protected HeuristicState parentState;
+ protected List<HeuristicState> childStates;
+
+ protected boolean isPathSensitive = false;
+
+ /*
+ * do we use A* adaptation of state priorities, i.e. have a
+ * distance + cost heuristic (in this context, we just use the
+ * path length as the "distance")
+ */
+ protected boolean useAstar;
+
+ /*
+ * a beam search is a HeuristicSearch with a state queue that is reset at each
+ * search level (i.e. it doesn't hop between search levels when fetching the
+ * next state from the queue)
+ */
+ protected boolean isBeamSearch;
+
+
+ public HeuristicSearch (Config config, VM vm) {
+ super(config, vm);
+
+ useAstar = config.getBoolean("search.heuristic.astar");
+ isBeamSearch = config.getBoolean("search.heuristic.beam_search");
+ }
+
+
+ // add the current state to the queue
+ protected abstract HeuristicState queueCurrentState ();
+
+ // return the next queued state, which becomes the new parentState
+ // implementors can also reset or modify the queue
+ protected abstract HeuristicState getNextQueuedState ();
+
+ public abstract int getQueueSize();
+ public abstract boolean isQueueLimitReached();
+
+ public HeuristicState getParentState() {
+ return parentState;
+ }
+
+ public List<HeuristicState> getChildStates() {
+ return childStates;
+ }
+
+ public void setPathSensitive (boolean isPathSensitive) {
+ this.isPathSensitive = isPathSensitive;
+ }
+
+ void backtrackToParent () {
+ backtrack();
+
+ depth--;
+ notifyStateBacktracked();
+ }
+
+ /*
+ * generate the set of all child states for the current parent state
+ *
+ * overriding methods can use the return value to determine if they
+ * have to process the childStates, e.g. to compute priorities
+ * that require the whole set
+ *
+ * @returns false if this is cut short by a property termination or
+ * explicit termination request
+ */
+ protected boolean generateChildren () {
+
+ childStates = new ArrayList<HeuristicState>();
+
+ while (!done) {
+
+ if (!forward()) {
+ notifyStateProcessed();
+ return true;
+ }
+
+ depth++;
+ notifyStateAdvanced();
+
+ if (currentError != null){
+ notifyPropertyViolated();
+ if (hasPropertyTermination()) {
+ return false;
+ }
+
+ // note that we don't store the error state anymore, which means we
+ // might encounter it along different paths. However, this is probably
+ // what we want for search.multiple_errors.
+
+ } else {
+
+ if (!isEndState() && !isIgnoredState()) {
+ boolean isNewState = isNewState();
+
+ if (isNewState && depth >= depthLimit) {
+ // we can't do this before we actually generated the VM child state
+ // since we don't want to report DEPTH_CONSTRAINTs for parents
+ // that have only visited or end state children
+ notifySearchConstraintHit("depth limit reached: " + depthLimit);
+
+ } else if (isNewState || isPathSensitive) {
+
+ if (isQueueLimitReached()) {
+ notifySearchConstraintHit("queue limit reached: " + getQueueSize());
+ }
+
+ HeuristicState newHState = queueCurrentState();
+ if (newHState != null) {
+ childStates.add(newHState);
+ notifyStateStored();
+ }
+ }
+
+ } else {
+ // end state or ignored transition
+ }
+ }
+
+ backtrackToParent();
+ }
+
+ return false;
+ }
+
+
+ private void restoreState (HeuristicState hState) {
+ vm.restoreState(hState.getVMState());
+
+ // note we have to query the depth from the VM because the state is taken from the queue
+ // and we have no idea when it was entered there
+ depth = vm.getPathLength();
+ notifyStateRestored();
+ }
+
+ @Override
+ public void search () {
+
+ queueCurrentState();
+ notifyStateStored();
+
+ // kind of stupid, but we need to get it out of the queue, and we
+ // don't have to restore it since it's the first one
+ parentState = getNextQueuedState();
+
+ done = false;
+ notifySearchStarted();
+
+ if (!hasPropertyTermination()) {
+ generateChildren();
+
+ while (!done && (parentState = getNextQueuedState()) != null) {
+ restoreState(parentState);
+
+ generateChildren();
+ }
+ }
+
+ notifySearchFinished();
+ }
+
+ @Override
+ public boolean supportsBacktrack () {
+ // we don't do multi-level backtracks, but automatically do backtrackToParent()
+ // after each child state generation
+ return false;
+ }
+}
+
+