gov.nasa.jpf.listener

Class NoStateCycles

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.listener.NoStateCycles

All Implemented Interfaces:

JPFListener, Property, PublisherExtension, SearchListener, Printable, VMListener

public class NoStateCycles
extends PropertyListenerAdapter

If there is a cycle in the states of the program, JPF doesn't execute the already visited states. A cycle in the states may represent the ability for the program to hang. This property finds and outputs cycles in the states so that they may be investigated. The following might need to be added to listener property... gov.nasa.jpf.tools.SimpleIdleFilter gov.nasa.jpf.tools.IdleFilter

Constructor Summary

Constructors

Constructor and Description
NoStateCycles(Config config)

Method Summary

Methods

Modifier and Type	Method and Description
boolean	check(Search search, VM vm) return true if property is NOT violated
String	getErrorMessage()
String	getExplanation()
void	reset()
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

Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter

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

Methods inherited from class gov.nasa.jpf.GenericProperty

printOn

Methods inherited from class java.lang.Object

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

Constructor Detail

NoStateCycles

public NoStateCycles(Config config)

Method Detail

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 PropertyListenerAdapter

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 PropertyListenerAdapter

check

public boolean check(Search search,
            VM vm)

Description copied from interface: Property

return true if property is NOT violated

Specified by:

check in interface Property

Overrides:

check in class PropertyListenerAdapter

reset

public void reset()

Specified by:

reset in interface Property

Overrides:

reset in class PropertyListenerAdapter

getErrorMessage

public String getErrorMessage()

Specified by:

getErrorMessage in interface Property

Overrides:

getErrorMessage in class GenericProperty

getExplanation

public String getExplanation()

Specified by:

getExplanation in interface Property

Overrides:

getExplanation in class GenericProperty