gov.nasa.jpf.search.heuristic

Class SimplePriorityHeuristic

java.lang.Object

gov.nasa.jpf.search.Search

gov.nasa.jpf.search.heuristic.HeuristicSearch

gov.nasa.jpf.search.heuristic.SimplePriorityHeuristic

Direct Known Subclasses:

BFSHeuristic, DFSHeuristic, GlobalSwitchThread, Interleaving, MinimizePreemption, MostBlocked, PreferThreads, RandomHeuristic, UserHeuristic

public abstract class SimplePriorityHeuristic
extends HeuristicSearch

a heuristic that is based on static priorities that are determined at state storage time

Field Summary

Fields

Modifier and Type	Field and Description
protected Predicate<ThreadInfo>	aliveThread

Fields inherited from class gov.nasa.jpf.search.heuristic.HeuristicSearch

childStates, isBeamSearch, isPathSensitive, parentState, 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
SimplePriorityHeuristic(Config config, VM vm)

Method Summary

Modifier and Type	Method and Description
protected int	computeAstarPathCost(VM vm)
protected abstract int	computeHeuristicValue()
protected HeuristicState	getNextQueuedState()
int	getQueueSize()
boolean	isQueueLimitReached()
protected HeuristicState	queueCurrentState()

Methods inherited from class gov.nasa.jpf.search.heuristic.HeuristicSearch

generateChildren, getChildStates, getParentState, search, setPathSensitive, 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

aliveThread

protected Predicate<ThreadInfo> aliveThread

Constructor Detail

SimplePriorityHeuristic

public SimplePriorityHeuristic(Config config,
                               VM vm)

Method Detail

computeHeuristicValue

protected abstract int computeHeuristicValue()

computeAstarPathCost

protected int computeAstarPathCost(VM vm)

queueCurrentState

protected HeuristicState queueCurrentState()

Specified by:

queueCurrentState in class HeuristicSearch

getNextQueuedState

protected HeuristicState getNextQueuedState()

Specified by:

getNextQueuedState in class HeuristicSearch

getQueueSize

public int getQueueSize()

Specified by:

getQueueSize in class HeuristicSearch

isQueueLimitReached

public boolean isQueueLimitReached()

Specified by:

isQueueLimitReached in class HeuristicSearch