gov.nasa.jpf.listener

Class DistributedSimpleDot

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.SimpleDot

gov.nasa.jpf.listener.DistributedSimpleDot

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

public class DistributedSimpleDot
extends SimpleDot

This is a Graphviz dot-file generator similar to SimpleDot. It is useful in the case of Multiprocess applications. It distinguishes local choices from global choices.

Field Summary

Fields

Modifier and Type	Field and Description
protected Instruction	insn
protected java.lang.String	mpNodeAttrs
protected java.lang.String	mpStartNodeAttrs

Fields inherited from class gov.nasa.jpf.listener.SimpleDot

app, backtrackEdgeAttrs, endNodeAttrs, errorNodeAttrs, file, genericEdgeAttrs, genericNodeAttrs, graphAttrs, lastEi, lastErrorId, lastId, lastTi, newEdgeAttrs, printFile, pw, restoreEdgeAttrs, showTarget, startNodeAttrs, visitedEdgeAttrs, vm

Constructor Summary

Constructors

Constructor and Description
DistributedSimpleDot(Config config, JPF jpf)

Method Summary

Modifier and Type	Method and Description
protected java.lang.String	getLastChoice()
protected java.lang.String	getNativeExecCG(EXECUTENATIVE insn)
protected java.lang.String	getNextCG()
void	instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nextInstruction, Instruction executedInstruction) VM has executed the next instruction (can be used to analyze branches, monitor PUTFIELD / GETFIELD and INVOKExx / RETURN instructions)
protected void	printMultiProcessState(java.lang.String stateId)
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.listener.SimpleDot

getClassObjectRef, getError, getFieldAccessCG, getInstanceRef, getInvokeCG, getLockCG, getStateId, objectWait, printBacktrack, printEndState, printErrorState, printHeader, printRestored, printStartState, printTransition, publishFinished, searchFinished, searchStarted, stateBacktracked, stateRestored, threadStarted

Methods inherited from class gov.nasa.jpf.ListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcBegin, gcEnd, loadClass, methodEntered, methodExited, objectCreated, objectExposed, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectShared, objectUnlocked, propertyViolated, publishConstraintHit, publishProbe, publishPropertyViolation, publishStart, publishTransition, searchConstraintHit, searchProbed, stateProcessed, statePurged, 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

Field Detail

mpNodeAttrs

protected java.lang.String mpNodeAttrs

mpStartNodeAttrs

protected java.lang.String mpStartNodeAttrs

insn

protected Instruction insn

Constructor Detail

DistributedSimpleDot

public DistributedSimpleDot(Config config,
                            JPF jpf)

Method Detail

instructionExecuted

public void instructionExecuted(VM vm,
                                ThreadInfo currentThread,
                                Instruction nextInstruction,
                                Instruction executedInstruction)

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

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 SimpleDot

getNextCG

protected java.lang.String getNextCG()

Overrides:

getNextCG in class SimpleDot

printMultiProcessState

protected void printMultiProcessState(java.lang.String stateId)

getNativeExecCG

protected java.lang.String getNativeExecCG(EXECUTENATIVE insn)

Overrides:

getNativeExecCG in class SimpleDot

getLastChoice

protected java.lang.String getLastChoice()

Overrides:

getLastChoice in class SimpleDot