gov.nasa.jpf.search

Class DFSearch

java.lang.Object

gov.nasa.jpf.search.Search

gov.nasa.jpf.search.DFSearch

public class DFSearch
extends Search

standard depth first model checking (but can be bounded by search depth and/or explicit Verify.ignoreIf)

Field Summary

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
DFSearch(Config config, VM vm)

Method Summary

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() state model of the search next new -> action T T forward T F backtrack, forward F T backtrack, forward F F backtrack, forward end condition backtrack failed (no saved states) | property violation (currently only checked in new states) | search constraint (depth or memory or time) <2do> we could split the properties into forward and backtrack properties, the latter ones being usable for liveness properties that are basically condition accumulators for sub-paths of the state space, to be checked when we backtrack to the state where they were introduced.
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, 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

DFSearch

public DFSearch(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()

state model of the search next new -> action T T forward T F backtrack, forward F T backtrack, forward F F backtrack, forward end condition backtrack failed (no saved states) | property violation (currently only checked in new states) | search constraint (depth or memory or time) <2do> we could split the properties into forward and backtrack properties, the latter ones being usable for liveness properties that are basically condition accumulators for sub-paths of the state space, to be checked when we backtrack to the state where they were introduced.

Specified by:

search in class Search

supportsBacktrack

public boolean supportsBacktrack()

Overrides:

supportsBacktrack in class Search