gov.nasa.jpf.listener

Class PathOutputMonitor

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.listener.PathOutputMonitor

All Implemented Interfaces:

JPFListener, Property, PublisherExtension, SearchListener, Printable, VMListener, java.lang.Cloneable

public class PathOutputMonitor
extends PropertyListenerAdapter

listener that monitors path output, matching it against specifications supplied as text files. Per default, this uses simple line-by-line regular expression matching, also supporting prefixes by means of special ". . ." ellipsis patterns. Each file can contain a number of path output specs, separated by "~~~~~" lines. The major purpose of this listener is to verify JPF state spaces, but it can also be used as a functional property

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static interface	PathOutputMonitor.PathOutputSpec

Constructor Summary

Constructors

Constructor and Description
PathOutputMonitor(Config config, JPF jpf)

Method Summary

Modifier and Type	Method and Description
boolean	check(Search search, VM vm) return true if property is NOT violated
java.lang.String	getErrorMessage()
void	publishFinished(Publisher publisher)
void	reset()
void	searchFinished(Search search) we're done, either with or without a preceeding error
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.PropertyListenerAdapter

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

Methods inherited from class gov.nasa.jpf.GenericProperty

getExplanation, printOn

Methods inherited from class java.lang.Object

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

Constructor Detail

PathOutputMonitor

public PathOutputMonitor(Config config,
                         JPF jpf)

Method Detail

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

getErrorMessage

public java.lang.String getErrorMessage()

Specified by:

getErrorMessage in interface Property

Overrides:

getErrorMessage in class GenericProperty

reset

public void reset()

Specified by:

reset in interface Property

Overrides:

reset in class PropertyListenerAdapter

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

searchFinished

public void searchFinished(Search search)

Description copied from interface: SearchListener

we're done, either with or without a preceeding error

Specified by:

searchFinished in interface SearchListener

Overrides:

searchFinished in class PropertyListenerAdapter

publishFinished

public void publishFinished(Publisher publisher)

Specified by:

publishFinished in interface PublisherExtension

Overrides:

publishFinished in class PropertyListenerAdapter