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

java.lang.Object
  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]