gov.nasa.jpf.search.heuristic

Class NewHeuristicSearch

java.lang.Object

gov.nasa.jpf.search.Search

gov.nasa.jpf.search.heuristic.NewHeuristicSearch

Direct Known Subclasses:

NewSimplePriorityHeuristic

public abstract class NewHeuristicSearch
extends Search

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.

Field Summary

Fields

Modifier and Type	Field and Description
protected java.util.List<HeuristicState>	childStates
protected boolean	isBeamSearch
protected boolean	isPathSensitive
protected HeuristicState	parentState
protected boolean	useAstar

Fields inherited from class gov.nasa.jpf.search.Search

config, currentError, depth, depthLimit, doBacktrack, done, errors, getAllErrors, lastSearchConstraint, listeners, log, matchDepth, minFreeMemory, notifyProbeListeners, properties, reporter, stateDepth, vm

Constructor Summary

Constructors

Constructor and Description
NewHeuristicSearch(Config config, VM vm)

Method Summary

Modifier and Type	Method and Description
protected boolean	generateChildren()
java.util.List<HeuristicState>	getChildStates()
protected abstract HeuristicState	getNextQueuedState()
HeuristicState	getParentState()
abstract int	getQueueSize()
abstract boolean	isQueueLimitReached()
protected abstract HeuristicState	queueCurrentState()
void	search()
void	setPathSensitive(boolean isPathSensitive)
boolean	supportsBacktrack()

Methods inherited from class gov.nasa.jpf.search.Search

addListener, addProperty, backtrack, checkAndResetBacktrackRequest, checkAndResetProbeRequest, checkPropertyViolation, checkStateSpaceLimit, cleanUp, error, error, forward, getConfig, getCurrentError, getDepth, getDepthLimit, getErrors, getLastError, getLastSearchConstraint, getNextListenerOfType, getNumberOfErrors, getProperties, getPurgedStateId, getSearchConstraint, getSearchState, getStateDepth, getStateId, getTransition, getVM, hasErrors, hasListenerOfType, hasNextState, hasPropertyTermination, initialize, isDone, isEndState, isErrorState, isIgnoredState, isNewState, isProcessedState, isVisitedState, notifyPropertyViolated, notifySearchConstraintHit, notifySearchFinished, notifySearchProbed, notifySearchStarted, notifyStateAdvanced, notifyStateBacktracked, notifyStateProcessed, notifyStatePurged, notifyStateRestored, notifyStateStored, probeSearch, removeListener, removeProperty, requestBacktrack, resetProperties, restoreState, setDepthLimit, setIgnoredState, setReporter, setStateDepth, supportsRestoreState, terminate, transitionOccurred

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

parentState

protected HeuristicState parentState

childStates

protected java.util.List<HeuristicState> childStates

isPathSensitive

protected boolean isPathSensitive

useAstar

protected boolean useAstar

isBeamSearch

protected boolean isBeamSearch

Constructor Detail

NewHeuristicSearch

public NewHeuristicSearch(Config config,
                          VM vm)

Method Detail

queueCurrentState

protected abstract HeuristicState queueCurrentState()

getNextQueuedState

protected abstract HeuristicState getNextQueuedState()

getQueueSize

public abstract int getQueueSize()

isQueueLimitReached

public abstract boolean isQueueLimitReached()

getParentState

public HeuristicState getParentState()

getChildStates

public java.util.List<HeuristicState> getChildStates()

setPathSensitive

public void setPathSensitive(boolean isPathSensitive)

generateChildren

protected boolean generateChildren()

search

public void search()

Specified by:

search in class Search

supportsBacktrack

public boolean supportsBacktrack()

Overrides:

supportsBacktrack in class Search