org.objectweb.dsrg.sofa.cushion.jpfcheck
Class ProtocolListener

java.lang.Object
  extended by gov.nasa.jpf.GenericProperty
      extended by gov.nasa.jpf.PropertyListenerAdapter
          extended by org.objectweb.dsrg.sofa.cushion.jpfcheck.ProtocolListener
All Implemented Interfaces:
gov.nasa.jpf.JPFListener, gov.nasa.jpf.jvm.VMListener, gov.nasa.jpf.Property, gov.nasa.jpf.report.PublisherExtension, gov.nasa.jpf.search.SearchListener, gov.nasa.jpf.util.Printable

public class ProtocolListener
extends gov.nasa.jpf.PropertyListenerAdapter

Listener for JPF that monitors protocol-related events (method invoke and return) and notifies the BPChecker when any such event occurs.


Constructor Summary
ProtocolListener(org.ow2.dsrg.fm.origbp.DFSR.JPFTraverser tr, java.util.Map itf2class, java.util.Set serverItfs, java.lang.String[] events)
           
 
Method Summary
 java.lang.String getErrorMessage()
           
 java.util.Set getMethodNames()
          Returns names of methods that are monitored by JPF.
 boolean check(gov.nasa.jpf.search.Search search, gov.nasa.jpf.jvm.JVM vm)
           
 void instructionExecuted(gov.nasa.jpf.jvm.JVM vm)
           
 void searchFinished(gov.nasa.jpf.search.Search search)
           
 void stateAdvanced(gov.nasa.jpf.search.Search search)
           
 void stateBacktracked(gov.nasa.jpf.search.Search search)
           
 void stateProcessed(gov.nasa.jpf.search.Search search)
           
 
Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter
classLoaded, exceptionThrown, executeInstruction, gcBegin, gcEnd, choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorSet, objectCreated, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectUnlocked, objectWait, propertyViolated, publishFinished, publishPropertyViolation, publishStart, publishTransition, searchConstraintHit, searchStarted, stateRestored, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadStarted, threadTerminated, threadWaiting
 
Methods inherited from class gov.nasa.jpf.GenericProperty
getExplanation, printOn, reset
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

ProtocolListener

public ProtocolListener(org.ow2.dsrg.fm.origbp.DFSR.JPFTraverser tr,
                        java.util.Map itf2class,
                        java.util.Set serverItfs,
                        java.lang.String[] events)
Parameters:
itf2class - map of names of interfaces to names of classes that implement them.
serverItfs - list of names of fractal server interfaces.
events - list of events that should be passed to the BP checker.
Method Detail

getMethodNames

public java.util.Set getMethodNames()
Returns names of methods that are monitored by JPF.


stateAdvanced

public void stateAdvanced(gov.nasa.jpf.search.Search search)
Specified by:
stateAdvanced in interface gov.nasa.jpf.search.SearchListener
Overrides:
stateAdvanced in class gov.nasa.jpf.PropertyListenerAdapter

stateBacktracked

public void stateBacktracked(gov.nasa.jpf.search.Search search)
Specified by:
stateBacktracked in interface gov.nasa.jpf.search.SearchListener
Overrides:
stateBacktracked in class gov.nasa.jpf.PropertyListenerAdapter

stateProcessed

public void stateProcessed(gov.nasa.jpf.search.Search search)
Specified by:
stateProcessed in interface gov.nasa.jpf.search.SearchListener
Overrides:
stateProcessed in class gov.nasa.jpf.PropertyListenerAdapter

searchFinished

public void searchFinished(gov.nasa.jpf.search.Search search)
Specified by:
searchFinished in interface gov.nasa.jpf.search.SearchListener
Overrides:
searchFinished in class gov.nasa.jpf.PropertyListenerAdapter

instructionExecuted

public void instructionExecuted(gov.nasa.jpf.jvm.JVM vm)
Specified by:
instructionExecuted in interface gov.nasa.jpf.jvm.VMListener
Overrides:
instructionExecuted in class gov.nasa.jpf.PropertyListenerAdapter

check

public boolean check(gov.nasa.jpf.search.Search search,
                     gov.nasa.jpf.jvm.JVM vm)
Specified by:
check in interface gov.nasa.jpf.Property
Overrides:
check in class gov.nasa.jpf.PropertyListenerAdapter

getErrorMessage

public java.lang.String getErrorMessage()
Specified by:
getErrorMessage in interface gov.nasa.jpf.Property
Overrides:
getErrorMessage in class gov.nasa.jpf.GenericProperty