edu.ksu.cis.projects.bogor.module
Class DefaultCounterExampleWriter.GuidedSearcherProxy

java.lang.Object
  extended by edu.ksu.cis.projects.bogor.module.DefaultCounterExampleWriter.GuidedSearcherProxy
All Implemented Interfaces:
DefaultCounterExampleWriter.IStateSnapshotSource, IModule, ISearcher, Disposable, InvocationHandler
Enclosing class:
DefaultCounterExampleWriter

protected class DefaultCounterExampleWriter.GuidedSearcherProxy
extends Object
implements ISearcher, DefaultCounterExampleWriter.IStateSnapshotSource, InvocationHandler

[Document Pending]

Version:
CVS $Revision: 1.44 $ $Date: 2005/06/09 00:22:01 $
Author:
$author$

Field Summary
protected  IBacktrackingInfoFactory bif
          [Document Pending]
protected  boolean externalizeAllStateInfo
          Flag controlling whether all states, transition sets, and next thread locations are externalized on the fly.
protected  IntStack recentlyMovedThreadIds
          Stack of thread descriptors corresponding to id of thread which executed each transition on DFS stack.
protected  List<ICounterExampleSchedulingInfo> schedulingDecisions
          The error path to reconstruct.
protected  int schedulingDecisionsToUse
          Execute the first X many steps of the counterexample trail.
protected  DefaultStateExternalizer se
          [Document Pending]
protected  DefaultCounterExampleWriter.GuidedSystemSharedState sharedSearchState
          Search metadata shared across all guided components.
protected  ISearcher sr
          [Document Pending]
protected  ISchedulingStrategist ss
          [Document Pending]
 
Fields inherited from interface edu.ksu.cis.projects.bogor.module.ISearcher
ASSERTION_FAILED_CODE, EXT_FAILED_CODE, ILL_FORMED_MODEL_CODE, INVALID_END_STATE_CODE, INVARIANT_VIOLATED_CODE, RANGE_EXCEPTION_CODE, UNCAUGHT_EXCEPTION_CODE
 
Constructor Summary
DefaultCounterExampleWriter.GuidedSearcherProxy(ISearcher sr, DefaultCounterExampleWriter.GuidedSystemSharedState gsss, List<ICounterExampleSchedulingInfo> schedulingDecisions)
          Creates a new GuidedSearcherProxy object.
DefaultCounterExampleWriter.GuidedSearcherProxy(ISearcher sr, DefaultCounterExampleWriter.GuidedSystemSharedState gsss, List<ICounterExampleSchedulingInfo> schedulingDecisions, int schedulingDecisionsToUse, boolean externalizeAllData)
          Creates a new GuidedSearcherProxy object.
 
Method Summary
 boolean backtrack()
          [Document Pending]
 IMessageStore connect(IBogorConfiguration bc)
          [Document Pending]
 IState createInitialState()
          [Document Pending]
 void dispose()
          [Document Pending]
 void doTransition(int threadId, Transformation t, Action a)
          [Document Pending]
 void error(int errCode)
          [Document Pending]
protected  void externalizeEnabledTransitions(IState state, int[] threadIds, Transformation[] transformations)
          [Document Pending]
protected  void externalizeNextMovedThread(IState state, int threadId, Transformation t)
          [Document Pending]
protected  void externalizeState(String stateId)
          [Document Pending]
 ArrayList<IBacktrackingInfo> getBacktrackingInfos()
          [Document Pending]
 String getCopyrightNotice()
          [Document Pending]
 String getEnabledTransitions()
          Get the set of enabled transitions at time of snapshot.
 int getErrorCount()
          [Document Pending]
protected  Location getLocation(int locDesc)
          [Document Pending]
 String getNextMovedThread()
          Get the transition set to be executed next at time of snapshot.
 IState getState()
          [Document Pending]
 String getStateSnapshot()
          Get state at time of snapshot.
 void initialize()
          [Document Pending]
 Object invoke(Object receiver, Method m, Object[] args)
          [Document Pending]
 void search()
          [Document Pending]
 IMessageStore setOptions(String key, Properties configuration)
          [Document Pending]
 boolean shouldStore()
          [Document Pending]
 boolean step()
          [Document Pending]
 boolean stepBackward()
          [Document Pending]
 boolean store()
          [Document Pending]
 void writeCounterExamples()
          [Document Pending]
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

se

protected DefaultStateExternalizer se
[Document Pending]


sr

protected ISearcher sr
[Document Pending]


ss

protected ISchedulingStrategist ss
[Document Pending]


bif

protected IBacktrackingInfoFactory bif
[Document Pending]


schedulingDecisions

protected List<ICounterExampleSchedulingInfo> schedulingDecisions
The error path to reconstruct.


externalizeAllStateInfo

protected boolean externalizeAllStateInfo
Flag controlling whether all states, transition sets, and next thread locations are externalized on the fly.


schedulingDecisionsToUse

protected int schedulingDecisionsToUse
Execute the first X many steps of the counterexample trail.


sharedSearchState

protected DefaultCounterExampleWriter.GuidedSystemSharedState sharedSearchState
Search metadata shared across all guided components.


recentlyMovedThreadIds

protected IntStack recentlyMovedThreadIds
Stack of thread descriptors corresponding to id of thread which executed each transition on DFS stack.

Constructor Detail

DefaultCounterExampleWriter.GuidedSearcherProxy

public DefaultCounterExampleWriter.GuidedSearcherProxy(ISearcher sr,
                                                       DefaultCounterExampleWriter.GuidedSystemSharedState gsss,
                                                       List<ICounterExampleSchedulingInfo> schedulingDecisions)
Creates a new GuidedSearcherProxy object.

Parameters:
sr - [Document Pending]

DefaultCounterExampleWriter.GuidedSearcherProxy

public DefaultCounterExampleWriter.GuidedSearcherProxy(ISearcher sr,
                                                       DefaultCounterExampleWriter.GuidedSystemSharedState gsss,
                                                       List<ICounterExampleSchedulingInfo> schedulingDecisions,
                                                       int schedulingDecisionsToUse,
                                                       boolean externalizeAllData)
Creates a new GuidedSearcherProxy object.

Parameters:
sr - [Document Pending]
Method Detail

getBacktrackingInfos

public ArrayList<IBacktrackingInfo> getBacktrackingInfos()
[Document Pending]

Specified by:
getBacktrackingInfos in interface ISearcher
Returns:
[Document Pending]

getCopyrightNotice

public String getCopyrightNotice()
[Document Pending]

Specified by:
getCopyrightNotice in interface IModule
Returns:
[Document Pending]

getEnabledTransitions

public String getEnabledTransitions()
Description copied from interface: DefaultCounterExampleWriter.IStateSnapshotSource
Get the set of enabled transitions at time of snapshot.

Specified by:
getEnabledTransitions in interface DefaultCounterExampleWriter.IStateSnapshotSource
Returns:
a string that can be parsed into a Transitions data binding from the CEF-XML package.

getErrorCount

public int getErrorCount()
[Document Pending]

Specified by:
getErrorCount in interface ISearcher
Returns:
[Document Pending]

getNextMovedThread

public String getNextMovedThread()
Description copied from interface: DefaultCounterExampleWriter.IStateSnapshotSource
Get the transition set to be executed next at time of snapshot.

Specified by:
getNextMovedThread in interface DefaultCounterExampleWriter.IStateSnapshotSource
Returns:
a string that can be parsed into a Transitions data binding from the CEF-XML package.

setOptions

public IMessageStore setOptions(String key,
                                Properties configuration)
[Document Pending]

Specified by:
setOptions in interface IModule
Parameters:
key - [Document Pending]
configuration - [Document Pending]

getState

public IState getState()
[Document Pending]

Specified by:
getState in interface ISearcher
Returns:
[Document Pending]

getStateSnapshot

public String getStateSnapshot()
Description copied from interface: DefaultCounterExampleWriter.IStateSnapshotSource
Get state at time of snapshot.

Specified by:
getStateSnapshot in interface DefaultCounterExampleWriter.IStateSnapshotSource
Returns:
a string that can be parsed into a StateType data binding from the CEF-XML package.

backtrack

public boolean backtrack()
[Document Pending]

Specified by:
backtrack in interface ISearcher
Returns:
[Document Pending]

connect

public IMessageStore connect(IBogorConfiguration bc)
[Document Pending]

Specified by:
connect in interface IModule
Parameters:
bc - [Document Pending]

createInitialState

public IState createInitialState()
[Document Pending]

Specified by:
createInitialState in interface ISearcher
Returns:
The initial state. Non-null.

dispose

public void dispose()
[Document Pending]

Specified by:
dispose in interface Disposable

doTransition

public void doTransition(int threadId,
                         Transformation t,
                         Action a)
[Document Pending]

Specified by:
doTransition in interface ISearcher
Parameters:
threadId - [Document Pending]
t - [Document Pending]
a - [Document Pending]

error

public void error(int errCode)
[Document Pending]

Specified by:
error in interface ISearcher
Parameters:
errCode - [Document Pending]

initialize

public void initialize()
[Document Pending]

Specified by:
initialize in interface ISearcher

invoke

public Object invoke(Object receiver,
                     Method m,
                     Object[] args)
[Document Pending]

Specified by:
invoke in interface InvocationHandler
Parameters:
receiver - [Document Pending]
m - [Document Pending]
args - [Document Pending]
Returns:
[Document Pending]

search

public void search()
[Document Pending]

Specified by:
search in interface ISearcher

shouldStore

public boolean shouldStore()
[Document Pending]

Specified by:
shouldStore in interface ISearcher
Returns:
[Document Pending]

step

public boolean step()
[Document Pending]

Specified by:
step in interface ISearcher
Returns:
[Document Pending]

stepBackward

public boolean stepBackward()
[Document Pending]

Specified by:
stepBackward in interface ISearcher
Returns:
[Document Pending]

store

public boolean store()
[Document Pending]

Specified by:
store in interface ISearcher
Returns:
[Document Pending]

writeCounterExamples

public void writeCounterExamples()
[Document Pending]

Specified by:
writeCounterExamples in interface ISearcher

getLocation

protected Location getLocation(int locDesc)
[Document Pending]

Parameters:
locDesc - [Document Pending]
Returns:
[Document Pending]

externalizeEnabledTransitions

protected void externalizeEnabledTransitions(IState state,
                                             int[] threadIds,
                                             Transformation[] transformations)
[Document Pending]

Parameters:
threadIds - [Document Pending]
transformations - [Document Pending]

externalizeNextMovedThread

protected void externalizeNextMovedThread(IState state,
                                          int threadId,
                                          Transformation t)
[Document Pending]

Parameters:
threadId - [Document Pending]
t - [Document Pending]

externalizeState

protected void externalizeState(String stateId)
[Document Pending]

Parameters:
stateId - [Document Pending]