Uses of Interface
gov.nasa.jpf.JPFListener

Packages that use JPFListener

Package	Description
gov.nasa.jpf
gov.nasa.jpf.listener
gov.nasa.jpf.report
gov.nasa.jpf.search
gov.nasa.jpf.util
gov.nasa.jpf.util.script
gov.nasa.jpf.vm
gov.nasa.jpf.vm.serialize

Uses of JPFListener in gov.nasa.jpf

Classes in gov.nasa.jpf that implement JPFListener

Modifier and Type	Class and Description
class	ListenerAdapter Adapter class that dummy implements both VMListener and SearchListener interfaces Used to ease implementation of listeners that only process a few notifications
class	PropertyListenerAdapter abstract base class that dummy implements Property, Search- and VMListener methods convenient for creating listeners that act as properties, just having to override the methods they need the only local functionality is that instances register themselves automatically as property when the search is started <2do> rewrite once GenericProperty is an interface

Methods in gov.nasa.jpf with parameters of type JPFListener

Modifier and Type	Method and Description
void	JPF.addListener(JPFListener l)
boolean	JPF.addUniqueTypeListener(JPFListener l)
void	JPF.removeListener(JPFListener l)

Uses of JPFListener in gov.nasa.jpf.listener

Classes in gov.nasa.jpf.listener that implement JPFListener

Modifier and Type	Class and Description
class	AssertionProperty this is a property listener that turns thrown AssertionErrors into property violations before they are caught (i.e.
class	BudgetChecker Listener that implements various budget constraints
class	CallMonitor this isn't yet a useful tool, but it shows how to track method calls with their corresponding argument values
class	CGMonitor
class	CGRemover listener that removes CGs for specified locations, method calls or method bodies This is an application specific state space optimizer that should be used carefully since it has to be aware of which CGs can be removed, and which ones can't (e.g.
class	ChoiceSelector this is a listener that only executes single choices until it detects that it should start to search.
class	ChoiceTracker generic choice tracker tool, to produce a list of choice values that can be used to create readable replay scripts etc.
class	CoverageAnalyzer a listener to report coverage statistics The idea is to collect per-class/-method/-thread information about executed instructions, and then analyze this deeper when it comes to report time (e.g.
class	DeadlockAnalyzer example of a listener that creates property specific traces.
class	EndlessLoopDetector little listener that tries to detect endless while() loops by counting backjumps, breaking transitions if the count exceeds a threshold, and then checking if program states match.
class	ErrorTraceGenerator A lightweight listener to generate the error trace by printing the program instructions at transition boundaries.
class	ExceptionInjector listener to inject exceptions according to user specifications.
class	ExecTracker Listener tool to monitor JPF execution.
class	HeapTracker HeapTracker - property-listener class to check heap utilization along all execution paths (e.g.
class	IdleFilter simple combined listener that checks if a thread seems to do idle loops that might starve other threads or JPF.
class	InsnCounter simple tools to gather statistics about instructions executed by JPF.
class	LockedStackDepth A listener that tracks information about the stack depth of when a lock is first acquired.
class	MethodAnalyzer analyzes call/execute sequences of methods closely modeled after the DeadlockAnalyzer, i.e.
class	MethodTracker simple tool to log method invocations at this point, it doesn't do fancy things yet, but gives a more high level idea of what got executed by JPF than the ExecTracker
class	NoStateCycles If there is a cycle in the states of the program, JPF doesn't execute the already visited states.
class	NumericValueChecker little listener that checks value ranges of specified numeric fields and local vars configuration examples: range.fields=speed,..
class	ObjectTracker listener that keeps track of all allocations, method calls, field updates and deallocations of instances of a set of types we don't need a StateExtensionClient/Listener here because we only keep live, typed object data.
class	OOMEInjector simulator for OutOfMemoryErrors.
class	OverlappingMethodAnalyzer this is a specialized MethodAnalyzer that looks for overlapping method calls on the same object from different threads.
class	PathOutputMonitor listener that monitors path output, matching it against specifications supplied as text files.
class	Perturbator listener that perturbs GETFIELD/GETSTATIC and InvokeInstruction results NOTE - this listener initializes in two steps: (1) during listener construction it builds a list of classes it has to monitor, and (2) during class load time it further analyzes classes from this list to get the actual target objects (FieldInfos and MethodInfos) so that instruction monitoring is efficient enough.
class	PreciseRaceDetector This is a Race Detection Algorithm that is precise in its calculation of races, i.e.
class	ReferenceLocator tiny utility listener that can be used to find out where a certain object (specified by reference) gets allocated or accessed (call or field), and when it gets gc'ed
class	SearchMonitor SearchListener class to collect and report statistical data during JPF execution.
class	SearchStats An alternative to SearchMonitor that just reports statistics at the end.
class	SimpleDot an alternative Graphviz dot-file generator for simple,educational state graphs except of creating funny wallpapers, it doesn't help much in real life if the state count gets > 50, but for the small ones it's actually quite readable.
class	SimpleIdleFilter This is the simple version of IdleFilter.
class	StackDepthChecker listener that throws a java.lang.StackOverflowError in case a thread exceeds a configured max stack depth <2do> - maybe we should only count visible stackframes, i.e.
class	StackTracker simple tool to log stack invocations at this point, it doesn't do fancy things yet, but gives a more high level idea of what got executed by JPF than the ExecTracker
class	StateCountEstimator From already visited states, estimates the total number of states by the branching factor.
class	StateSpaceAnalyzer a listener that collects information about ChoiceGenerators, choices and where they are used.
class	StateSpaceDot
class	StateTracker simple tool to log state changes
class	StopWatchFuzzer a listener that is used to explore all paths from a time-value comparison.
class	TraceStorer tool to save traces upon various conditions like - property violation - call of a certain method - reaching a certain search depth - creating a certain thread
class	VarRecorder Simple listener tool to record the values of variables as they are accessed.
class	VarTracker simple listener tool to find out which variables (locals and fields) are changed how often and from where.

Uses of JPFListener in gov.nasa.jpf.report

Classes in gov.nasa.jpf.report that implement JPFListener

Modifier and Type	Class and Description
class	Reporter this is our default report generator, which is heavily configurable via our standard properties.
class	Statistics simple structure to hold statistics info created by Reporters/Publishers this is kind of a second tier SearchListener, which does not explicitly have to be registered <2do> this should get generic and accessible enough to replace all the other statistics collectors, otherwise there is too much redundancy.

Uses of JPFListener in gov.nasa.jpf.search

Subinterfaces of JPFListener in gov.nasa.jpf.search

Modifier and Type	Interface and Description
interface	SearchListener interface to register for notification by the Search object.

Classes in gov.nasa.jpf.search that implement JPFListener

Modifier and Type	Class and Description
class	SearchListenerAdapter a no-action SearchListener which we can use to override only the notifications we are interested in

Uses of JPFListener in gov.nasa.jpf.util

Classes in gov.nasa.jpf.util that implement JPFListener

Modifier and Type	Class and Description
class	StateExtensionListener<T> generic listener that keeps track of state extensions, using state ids as index values into a dynamic array of T objects the purpose of this utility class is to make state extensions backtrackable, so that clients don't have to care about this
class	Trace<T> a generic, listener- created trace over property specific operations we could register this as a listener itself, but since it usually is used from a listener, we might as well just delegate from there

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

Classes in gov.nasa.jpf.util.script that implement JPFListener

Modifier and Type	Class and Description
class	EventGeneratorFactory abstract root for backtrackable event generator factories <2do> - we don't support backtracking for sections yet! needs to be implemented for state charts

Uses of JPFListener in gov.nasa.jpf.vm

Subinterfaces of JPFListener in gov.nasa.jpf.vm

Modifier and Type	Interface and Description
interface	VMListener interface to register for callbacks by the VM Observer role in equally named pattern Note that we only have notifications for generic events, NOT for conditions that are property specific, and especially nothing that is just triggered from an extension.

Classes in gov.nasa.jpf.vm that implement JPFListener

Modifier and Type	Class and Description
class	ConstInsnPathTime time model that uses instruction count along current path to deduce the execution time.

Methods in gov.nasa.jpf.vm with parameters of type JPFListener

Modifier and Type	Method and Description
void	MJIEnv.addListener(JPFListener l)
void	MJIEnv.removeListener(JPFListener l)

Uses of JPFListener in gov.nasa.jpf.vm.serialize

Classes in gov.nasa.jpf.vm.serialize that implement JPFListener

Modifier and Type	Class and Description
class	DynamicAbstractionSerializer.Attributor