gov.nasa.jpf.report

Class Statistics

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.report.Statistics

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener, Cloneable

public class Statistics
extends ListenerAdapter
implements Cloneable

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. If users have special requirements, they should subclass Statistics and set jpf.report.statistics.class accordingly Note that Statistics might be accessed by a background thread reporting JPF progress, hence we have to synchronize

Field Summary

Fields

Modifier and Type	Field and Description
long	backtracked
int	constraints
int	dataCGs
long	endStates
int	gcCycles
long	insns
int	maxDepth
int	maxLiveObjects
long	maxUsed
int	monitorCGs
long	newStates
long	nNewObjects
long	nReleasedObjects
int	processed
long	restored
int	sharedAccessCGs
int	signalCGs
int	threadCGs
long	visitedStates

Constructor Summary

Constructors

Constructor and Description
Statistics()

Method Summary

Methods

Modifier and Type	Method and Description
void	choiceGeneratorSet(VM vm, ChoiceGenerator<?> newCG) a new ChoiceGenerator was set, which means we are at the beginning of a new transition.
Statistics	clone()
void	gcBegin(VM vm)
void	instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) VM has executed the next instruction (can be used to analyze branches, monitor PUTFIELD / GETFIELD and INVOKExx / RETURN instructions)
void	objectCreated(VM vm, ThreadInfo ti, ElementInfo ei) new object was created
void	objectReleased(VM vm, ThreadInfo ti, ElementInfo ei) object was garbage collected (after potential finalization)
void	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	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	stateBacktracked(Search search) state was backtracked one step
void	stateProcessed(Search search) state is fully explored
void	stateRestored(Search search) a previously generated state was restored (can be on a completely different path)

Methods inherited from class gov.nasa.jpf.ListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, classLoaded, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcEnd, loadClass, methodEntered, methodExited, objectLocked, objectNotify, objectNotifyAll, objectUnlocked, objectWait, propertyViolated, publishConstraintHit, publishFinished, publishPropertyViolation, publishStart, publishTransition, searchFinished, searchStarted, statePurged, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadStarted, threadTerminated, threadWaiting, vmInitialized

Methods inherited from class java.lang.Object

equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

maxUsed

public long maxUsed

newStates

public long newStates

backtracked

public long backtracked

restored

public long restored

processed

public int processed

constraints

public int constraints

visitedStates

public long visitedStates

endStates

public long endStates

maxDepth

public int maxDepth

gcCycles

public int gcCycles

insns

public long insns

threadCGs

public int threadCGs

sharedAccessCGs

public int sharedAccessCGs

monitorCGs

public int monitorCGs

signalCGs

public int signalCGs

dataCGs

public int dataCGs

nNewObjects

public long nNewObjects

nReleasedObjects

public long nReleasedObjects

maxLiveObjects

public int maxLiveObjects

Constructor Detail

Statistics

public Statistics()

Method Detail

clone

public Statistics clone()

Overrides:

clone in class Object

gcBegin

public void gcBegin(VM vm)

Specified by:

gcBegin in interface VMListener

Overrides:

gcBegin in class ListenerAdapter

instructionExecuted

public void instructionExecuted(VM vm,
                       ThreadInfo ti,
                       Instruction nextInsn,
                       Instruction executedInsn)

Description copied from interface: VMListener

VM has executed the next instruction (can be used to analyze branches, monitor PUTFIELD / GETFIELD and INVOKExx / RETURN instructions)

Specified by:

instructionExecuted in interface VMListener

Overrides:

instructionExecuted in class ListenerAdapter

choiceGeneratorSet

public void choiceGeneratorSet(VM vm,
                      ChoiceGenerator<?> newCG)

Description copied from interface: VMListener

a new ChoiceGenerator was set, which means we are at the beginning of a new transition. NOTE - this notification happens before the KernelState is stored, i.e. listeners are NOT allowed to alter the KernelState (e.g. by changing field values or thread states)

Specified by:

choiceGeneratorSet in interface VMListener

Overrides:

choiceGeneratorSet in class ListenerAdapter

objectCreated

public void objectCreated(VM vm,
                 ThreadInfo ti,
                 ElementInfo ei)

Description copied from interface: VMListener

new object was created

Specified by:

objectCreated in interface VMListener

Overrides:

objectCreated in class ListenerAdapter

objectReleased

public void objectReleased(VM vm,
                  ThreadInfo ti,
                  ElementInfo ei)

Description copied from interface: VMListener

object was garbage collected (after potential finalization)

Specified by:

objectReleased in interface VMListener

Overrides:

objectReleased in class ListenerAdapter

stateAdvanced

public void stateAdvanced(Search search)

Description copied from interface: SearchListener

got the next state Note - this will be notified before any potential propertyViolated, in which case the currentError will be already set

Specified by:

stateAdvanced in interface SearchListener

Overrides:

stateAdvanced in class ListenerAdapter

stateBacktracked

public void stateBacktracked(Search search)

Description copied from interface: SearchListener

state was backtracked one step

Specified by:

stateBacktracked in interface SearchListener

Overrides:

stateBacktracked in class ListenerAdapter

stateProcessed

public void stateProcessed(Search search)

Description copied from interface: SearchListener

state is fully explored

Specified by:

stateProcessed in interface SearchListener

Overrides:

stateProcessed in class ListenerAdapter

stateRestored

public void stateRestored(Search search)

Description copied from interface: SearchListener

a previously generated state was restored (can be on a completely different path)

Specified by:

stateRestored in interface SearchListener

Overrides:

stateRestored in class ListenerAdapter

searchConstraintHit

public void searchConstraintHit(Search search)

Description copied from interface: SearchListener

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

Specified by:

searchConstraintHit in interface SearchListener

Overrides:

searchConstraintHit in class ListenerAdapter