gov.nasa.jpf.listener

Class ChoiceSelector

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.ChoiceSelector

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

public class ChoiceSelector
extends ListenerAdapter

this is a listener that only executes single choices until it detects that it should start to search. If nothing is specified, this is pretty much a simulator that randomly picks choices. Otherwise the user can give it any combination of - a set of thread names - a set of method names - a start search depth to turn on the search. If more than one condition is given, all have to be satisfied

Constructor Summary

Constructors

Constructor and Description
ChoiceSelector(Config config, JPF jpf)

Method Summary

Methods

Modifier and Type	Method and Description
void	choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) the next choice was requested from a previously registered ChoiceGenerator NOTE - this notification happens before the KernelState is stored, i.e.
void	executeInstruction(VM vm, ThreadInfo ti, Instruction insnToExecute) VM is about to execute the next instruction
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	threadStarted(VM vm, ThreadInfo ti) new Thread entered run() method

Methods inherited from class gov.nasa.jpf.ListenerAdapter

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

Methods inherited from class java.lang.Object

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

Constructor Detail

ChoiceSelector

public ChoiceSelector(Config config,
              JPF jpf)

Method Detail

choiceGeneratorAdvanced

public void choiceGeneratorAdvanced(VM vm,
                           ChoiceGenerator<?> currentCG)

Description copied from interface: VMListener

the next choice was requested from a previously registered ChoiceGenerator 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:

choiceGeneratorAdvanced in interface VMListener

Overrides:

choiceGeneratorAdvanced in class ListenerAdapter

threadStarted

public void threadStarted(VM vm,
                 ThreadInfo ti)

Description copied from interface: VMListener

new Thread entered run() method

Specified by:

threadStarted in interface VMListener

Overrides:

threadStarted in class ListenerAdapter

executeInstruction

public void executeInstruction(VM vm,
                      ThreadInfo ti,
                      Instruction insnToExecute)

Description copied from interface: VMListener

VM is about to execute the next instruction

Specified by:

executeInstruction in interface VMListener

Overrides:

executeInstruction 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