gov.nasa.jpf.listener

Class StateSpaceAnalyzer

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.StateSpaceAnalyzer

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

public class StateSpaceAnalyzer
extends ListenerAdapter
implements PublisherExtension

a listener that collects information about ChoiceGenerators, choices and where they are used. The purpose is to find out what causes the state space size, and to give hints of how to reduce it. The interesting part is that this is a listener that doesn't work off traces, but needs to collect info up to a point where we want it to report. That's state space or resource related, i.e. a combination of - number of transitions - memory consumption - elapsed time once the limit is reached, we stop the search and report. There are two parts we are interested in: - what CGs do we have - what creates those CGs (thread,insn,source) = last step insn

Constructor Summary

Constructors

Constructor and Description
StateSpaceAnalyzer(Config config, JPF jpf)

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.
void	publishFinished(Publisher publisher)
void	searchStarted(Search search) we get this after we enter the search loop, but BEFORE the first forward
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

Methods inherited from class gov.nasa.jpf.ListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, classLoaded, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcBegin, gcEnd, instructionExecuted, loadClass, methodEntered, methodExited, objectCreated, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectUnlocked, objectWait, propertyViolated, publishConstraintHit, publishPropertyViolation, publishStart, publishTransition, searchConstraintHit, searchFinished, stateBacktracked, stateProcessed, statePurged, stateRestored, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadStarted, threadTerminated, threadWaiting, vmInitialized

Methods inherited from class java.lang.Object

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

Methods inherited from interface gov.nasa.jpf.report.PublisherExtension

publishConstraintHit, publishPropertyViolation, publishStart, publishTransition

Constructor Detail

StateSpaceAnalyzer

public StateSpaceAnalyzer(Config config,
                  JPF jpf)

Method Detail

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

searchStarted

public void searchStarted(Search search)

Description copied from interface: SearchListener

we get this after we enter the search loop, but BEFORE the first forward

Specified by:

searchStarted in interface SearchListener

Overrides:

searchStarted 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

publishFinished

public void publishFinished(Publisher publisher)

Specified by:

publishFinished in interface PublisherExtension

Overrides:

publishFinished in class ListenerAdapter