gov.nasa.jpf.search

Class PathSearch

java.lang.Object

gov.nasa.jpf.search.Search

gov.nasa.jpf.search.PathSearch

public class PathSearch
extends Search

PathSearch is not really a Search object, just a simple 'forward' driver for the VM that loops until there is no next instruction or a property doesn't hold

Field Summary

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

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

Constructor Summary

Constructors

Constructor and Description
PathSearch(Config config, VM vm)

Method Summary

Methods

Modifier and Type	Method and Description
boolean	requestBacktrack() this is somewhat redundant to SystemState.setIgnored(), but we don't want to mix the case of overriding state matching with backtracking when searching for multiple errors
void	search()
boolean	supportsBacktrack()

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

addListener, addProperty, backtrack, checkAndResetBacktrackRequest, 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, notifySearchStarted, notifyStateAdvanced, notifyStateBacktracked, notifyStateProcessed, notifyStatePurged, notifyStateRestored, notifyStateStored, removeListener, removeProperty, 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

Constructor Detail

PathSearch

public PathSearch(Config config,
          VM vm)

Method Detail

requestBacktrack

public boolean requestBacktrack()

Description copied from class: Search

this is somewhat redundant to SystemState.setIgnored(), but we don't want to mix the case of overriding state matching with backtracking when searching for multiple errors

Overrides:

requestBacktrack in class Search

search

public void search()

Specified by:

search in class Search

supportsBacktrack

public boolean supportsBacktrack()

Overrides:

supportsBacktrack in class Search