Uses of Class gov.nasa.jpf.search.Search (JPF API)

Packages that use Search
Package	Description
gov.nasa.jpf
gov.nasa.jpf.listener
gov.nasa.jpf.report
gov.nasa.jpf.search
gov.nasa.jpf.search.heuristic
gov.nasa.jpf.util
gov.nasa.jpf.util.script
gov.nasa.jpf.vm

Uses of Search in gov.nasa.jpf

Methods in gov.nasa.jpf that return Search
Modifier and Type	Method and Description
`Search`	JPF.`getSearch()` return the search object.

Methods in gov.nasa.jpf with parameters of type Search
Modifier and Type	Method and Description
`boolean`	PropertyListenerAdapter.`check(Search search, VM vm)`
`boolean`	Property.`check(Search search, VM vm)` return true if property is NOT violated
`abstract boolean`	GenericProperty.`check(Search search, VM vm)`
`void`	PropertyListenerAdapter.`propertyViolated(Search search)`
`void`	ListenerAdapter.`propertyViolated(Search search)`
`void`	PropertyListenerAdapter.`searchConstraintHit(Search search)`
`void`	ListenerAdapter.`searchConstraintHit(Search search)`
`void`	PropertyListenerAdapter.`searchFinished(Search search)`
`void`	ListenerAdapter.`searchFinished(Search search)`
`void`	PropertyListenerAdapter.`searchStarted(Search search)`
`void`	ListenerAdapter.`searchStarted(Search search)`
`void`	PropertyListenerAdapter.`stateAdvanced(Search search)`
`void`	ListenerAdapter.`stateAdvanced(Search search)`
`void`	PropertyListenerAdapter.`stateBacktracked(Search search)`
`void`	ListenerAdapter.`stateBacktracked(Search search)`
`void`	PropertyListenerAdapter.`stateProcessed(Search search)`
`void`	ListenerAdapter.`stateProcessed(Search search)`
`void`	PropertyListenerAdapter.`statePurged(Search search)`
`void`	ListenerAdapter.`statePurged(Search search)`
`void`	PropertyListenerAdapter.`stateRestored(Search search)`
`void`	ListenerAdapter.`stateRestored(Search search)`
`void`	PropertyListenerAdapter.`stateStored(Search search)`
`void`	ListenerAdapter.`stateStored(Search search)`

Uses of Search in gov.nasa.jpf.listener

Methods in gov.nasa.jpf.listener with parameters of type Search
Modifier and Type	Method and Description
`boolean`	AssertionProperty.`check(Search search, VM vm)`
`boolean`	HeapTracker.`check(Search search, VM vm)` return 'false' if property is violated
`boolean`	EndlessLoopDetector.`check(Search search, VM vm)`
`boolean`	ObjectTracker.`check(Search search, VM vm)`
`boolean`	NoStateCycles.`check(Search search, VM vm)`
`boolean`	PathOutputMonitor.`check(Search search, VM vm)`
`boolean`	NumericValueChecker.`check(Search search, VM vm)`
`boolean`	PreciseRaceDetector.`check(Search search, VM vm)`
`protected String`	SimpleDot.`getError(Search search)`
`void`	ChoiceTracker.`propertyViolated(Search search)`
`void`	StateSpaceDot.`propertyViolated(Search search)`
`void`	SearchStats.`propertyViolated(Search search)`
`void`	SearchMonitor.`propertyViolated(Search search)`
`void`	ErrorTraceGenerator.`propertyViolated(Search search)`
`void`	TraceStorer.`propertyViolated(Search search)`
`void`	StateSpaceDot.`searchConstraintHit(Search search)`
`void`	SearchStats.`searchConstraintHit(Search search)`
`void`	SearchMonitor.`searchConstraintHit(Search search)`
`void`	TraceStorer.`searchConstraintHit(Search search)`
`void`	SimpleDot.`searchFinished(Search search)`
`void`	InsnCounter.`searchFinished(Search search)`
`void`	StateSpaceDot.`searchFinished(Search search)`
`void`	SearchStats.`searchFinished(Search search)`
`void`	StateCountEstimator.`searchFinished(Search search)`
`void`	PathOutputMonitor.`searchFinished(Search search)`
`void`	ExecTracker.`searchFinished(Search search)`
`void`	SearchMonitor.`searchFinished(Search search)`
`void`	MethodTracker.`searchFinished(Search search)`
`void`	StateTracker.`searchFinished(Search search)`
`void`	SimpleDot.`searchStarted(Search search)`
`void`	LockedStackDepth.`searchStarted(Search search)`
`void`	HeapTracker.`searchStarted(Search search)` SearchListener interface
`void`	StateSpaceDot.`searchStarted(Search search)`
`void`	SearchStats.`searchStarted(Search search)`
`void`	StateCountEstimator.`searchStarted(Search search)`
`void`	StateSpaceAnalyzer.`searchStarted(Search search)`
`void`	ExecTracker.`searchStarted(Search search)`
`void`	SearchMonitor.`searchStarted(Search search)`
`void`	MethodTracker.`searchStarted(Search search)`
`void`	StateTracker.`searchStarted(Search search)`
`void`	MethodAnalyzer.`stateAdvanced(Search search)`
`void`	SimpleDot.`stateAdvanced(Search search)`
`void`	LockedStackDepth.`stateAdvanced(Search search)`
`void`	IdleFilter.`stateAdvanced(Search search)`
`void`	HeapTracker.`stateAdvanced(Search search)`
`void`	DeadlockAnalyzer.`stateAdvanced(Search search)`
`void`	StateSpaceDot.`stateAdvanced(Search search)`
`void`	StackTracker.`stateAdvanced(Search search)`
`void`	CGMonitor.`stateAdvanced(Search search)`
`void`	ChoiceSelector.`stateAdvanced(Search search)`
`void`	SearchStats.`stateAdvanced(Search search)`
`void`	EndlessLoopDetector.`stateAdvanced(Search search)`
`void`	VarTracker.`stateAdvanced(Search search)`
`void`	StateSpaceAnalyzer.`stateAdvanced(Search search)`
`void`	NoStateCycles.`stateAdvanced(Search search)`
`void`	PathOutputMonitor.`stateAdvanced(Search search)`
`void`	ExecTracker.`stateAdvanced(Search search)`
`void`	BudgetChecker.`stateAdvanced(Search search)`
`void`	SearchMonitor.`stateAdvanced(Search search)`
`void`	SimpleIdleFilter.`stateAdvanced(Search search)`
`void`	MethodTracker.`stateAdvanced(Search search)`
`void`	StateTracker.`stateAdvanced(Search search)`
`void`	TraceStorer.`stateAdvanced(Search search)`
`void`	MethodAnalyzer.`stateBacktracked(Search search)`
`void`	SimpleDot.`stateBacktracked(Search search)`
`void`	LockedStackDepth.`stateBacktracked(Search search)`
`void`	IdleFilter.`stateBacktracked(Search search)`
`void`	HeapTracker.`stateBacktracked(Search search)`
`void`	DeadlockAnalyzer.`stateBacktracked(Search search)`
`void`	StateSpaceDot.`stateBacktracked(Search search)`
`void`	StackTracker.`stateBacktracked(Search search)`
`void`	CGMonitor.`stateBacktracked(Search search)`
`void`	SearchStats.`stateBacktracked(Search search)`
`void`	NoStateCycles.`stateBacktracked(Search search)`
`void`	ExecTracker.`stateBacktracked(Search search)`
`void`	SearchMonitor.`stateBacktracked(Search search)`
`void`	SimpleIdleFilter.`stateBacktracked(Search search)`
`void`	MethodTracker.`stateBacktracked(Search search)`
`void`	StateTracker.`stateBacktracked(Search search)`
`void`	LockedStackDepth.`stateProcessed(Search search)`
`void`	StateSpaceDot.`stateProcessed(Search search)`
`void`	SearchStats.`stateProcessed(Search search)`
`void`	StateCountEstimator.`stateProcessed(Search search)`
`void`	ExecTracker.`stateProcessed(Search search)`
`void`	SearchMonitor.`stateProcessed(Search search)`
`void`	MethodAnalyzer.`stateRestored(Search search)`
`void`	SimpleDot.`stateRestored(Search search)`
`void`	LockedStackDepth.`stateRestored(Search search)`
`void`	DeadlockAnalyzer.`stateRestored(Search search)`
`void`	StateSpaceDot.`stateRestored(Search search)`
`void`	CGMonitor.`stateRestored(Search search)`
`void`	SearchStats.`stateRestored(Search search)`
`void`	ExecTracker.`stateRestored(Search search)` SearchListener interface
`void`	SearchMonitor.`stateRestored(Search search)`
`void`	MethodTracker.`stateRestored(Search search)`
`void`	StateTracker.`stateRestored(Search search)`
`void`	MethodAnalyzer.`stateStored(Search search)`
`void`	DeadlockAnalyzer.`stateStored(Search search)`

Uses of Search in gov.nasa.jpf.report

Fields in gov.nasa.jpf.report declared as Search
Modifier and Type	Field and Description
`protected Search`	Reporter.`search`

Methods in gov.nasa.jpf.report that return Search
Modifier and Type	Method and Description
`Search`	Reporter.`getSearch()`

Methods in gov.nasa.jpf.report with parameters of type Search
Modifier and Type	Method and Description
`void`	Reporter.`propertyViolated(Search search)`
`void`	Reporter.`searchConstraintHit(Search search)`
`void`	Statistics.`searchConstraintHit(Search search)`
`void`	Reporter.`searchFinished(Search search)`
`void`	Reporter.`searchStarted(Search search)`
`void`	Reporter.`stateAdvanced(Search search)`
`void`	Statistics.`stateAdvanced(Search search)`
`void`	Statistics.`stateBacktracked(Search search)`
`void`	Statistics.`stateProcessed(Search search)`
`void`	Statistics.`stateRestored(Search search)`

Uses of Search in gov.nasa.jpf.search

Subclasses of Search in gov.nasa.jpf.search
Modifier and Type	Class and Description
`class`	`DFSearch` standard depth first model checking (but can be bounded by search depth and/or explicit Verify.ignoreIf)
`class`	`PathSearch` 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
`class`	`RandomSearch` this is a straight execution pseudo-search - it doesn't search at all (i.e.
`class`	`Simulation` this is a straight execution pseudo-search - it doesn't search at all (i.e.

Methods in gov.nasa.jpf.search with parameters of type Search
Modifier and Type	Method and Description
`void`	SearchListener.`propertyViolated(Search search)` JPF encountered a property violation.
`void`	SearchListenerAdapter.`propertyViolated(Search search)`
`void`	SearchListener.`searchConstraintHit(Search search)` there was some contraint hit in the search, we back out could have been turned into a property, but usually is an attribute of the search, not the application
`void`	SearchListenerAdapter.`searchConstraintHit(Search search)`
`void`	SearchListener.`searchFinished(Search search)` we're done, either with or without a preceeding error
`void`	SearchListenerAdapter.`searchFinished(Search search)`
`void`	SearchListener.`searchStarted(Search search)` we get this after we enter the search loop, but BEFORE the first forward
`void`	SearchListenerAdapter.`searchStarted(Search search)`
`void`	SearchListener.`stateAdvanced(Search search)` got the next state Note - this will be notified before any potential propertyViolated, in which case the currentError will be already set
`void`	SearchListenerAdapter.`stateAdvanced(Search search)`
`void`	SearchListener.`stateBacktracked(Search search)` state was backtracked one step
`void`	SearchListenerAdapter.`stateBacktracked(Search search)`
`void`	SearchListener.`stateProcessed(Search search)` state is fully explored
`void`	SearchListenerAdapter.`stateProcessed(Search search)`
`void`	SearchListener.`statePurged(Search search)` some state is not going to appear in any path anymore
`void`	SearchListenerAdapter.`statePurged(Search search)`
`void`	SearchListener.`stateRestored(Search search)` a previously generated state was restored (can be on a completely different path)
`void`	SearchListenerAdapter.`stateRestored(Search search)`
`void`	SearchListener.`stateStored(Search search)` somebody stored the state
`void`	SearchListenerAdapter.`stateStored(Search search)`

Uses of Search in gov.nasa.jpf.search.heuristic

Subclasses of Search in gov.nasa.jpf.search.heuristic
Modifier and Type	Class and Description
`class`	`BFSHeuristic` breadth first search
`class`	`DFSHeuristic` heuristic state prioritizer that favors search depth
`class`	`GlobalSwitchThread` heuristic state prioritizer that tries to minimize re-scheduling
`class`	`HeuristicSearch` 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.
`class`	`Interleaving` Heuristic to maximize thread interleavings.
`class`	`MinimizePreemption` a simple heuristic that tries to minimize preemptive scheduling, i.e.
`class`	`MostBlocked` Heuristic state prioriizer that maximizes number of blocked states.
`class`	`PreferThreads` a heuristic state prioritizer that favors certain threads (specified by thread names during initialization) <2do> for both efficiency and encapsulation reasons, this should be just a Scheduler policy (so that we don't have to expand all children)
`class`	`RandomHeuristic` heuristic state prioritizer that returns random priority values
`class`	`SimplePriorityHeuristic` a heuristic that is based on static priorities that are determined at state storage time
`class`	`UserHeuristic` heuristic state prioritizer that uses fields of the Main class under test to determine priorities (i.e.

Uses of Search in gov.nasa.jpf.util

Methods in gov.nasa.jpf.util with parameters of type Search
Modifier and Type	Method and Description
`void`	StateExtensionListener.`stateAdvanced(Search search)`
`void`	Trace.`stateAdvanced(Search search)`
`void`	StateExtensionListener.`stateBacktracked(Search search)`
`void`	Trace.`stateBacktracked(Search search)`
`void`	StateExtensionListener.`stateRestored(Search search)`
`void`	Trace.`stateRestored(Search search)`
`void`	Trace.`stateStored(Search search)`

Uses of Search in gov.nasa.jpf.util.script

Methods in gov.nasa.jpf.util.script with parameters of type Search
Modifier and Type	Method and Description
`void`	EventGeneratorFactory.`searchStarted(Search search)` SearchListener interface
`void`	EventGeneratorFactory.`stateAdvanced(Search search)`
`void`	EventGeneratorFactory.`stateBacktracked(Search search)`
`void`	EventGeneratorFactory.`stateRestored(Search search)`

Uses of Search in gov.nasa.jpf.vm

Methods in gov.nasa.jpf.vm with parameters of type Search
Modifier and Type	Method and Description
`boolean`	NotDeadlockedProperty.`check(Search search, VM vm)`
`boolean`	NoOutOfMemoryErrorProperty.`check(Search search, VM vm)`
`boolean`	NoUncaughtExceptionsProperty.`check(Search search, VM vm)`

Constructors in gov.nasa.jpf.vm with parameters of type Search
Constructor and Description
`NotDeadlockedProperty(Config conf, Search search)`

Uses of Classgov.nasa.jpf.search.Search

Uses of Search in gov.nasa.jpf

Uses of Search in gov.nasa.jpf.listener

Uses of Search in gov.nasa.jpf.report

Uses of Search in gov.nasa.jpf.search

Uses of Search in gov.nasa.jpf.search.heuristic

Uses of Search in gov.nasa.jpf.util

Uses of Search in gov.nasa.jpf.util.script

Uses of Search in gov.nasa.jpf.vm

Uses of Class
gov.nasa.jpf.search.Search