edu.ksu.cis.projects.bogor.module
Interface ISearcher

All Superinterfaces:

Disposable, IModule

All Known Implementing Classes:

DefaultCounterExampleWriter.GuidedSearcherProxy, DefaultSearcher

public interface ISearcher
extends IModule

This interface is the top-level interface for a state-space search algorithm.

Version:

CVS $Revision: 1.4 $ $Date: 2004/12/18 22:36:33 $

Author:

Robby

Field Summary

static int	ASSERTION_FAILED_CODE The error code for assertion failure.
static int	EXT_FAILED_CODE The error code for extension failure.
static int	ILL_FORMED_MODEL_CODE The error code for ill-formed model.
static int	INVALID_END_STATE_CODE The error code for invalid end state.
static int	INVARIANT_VIOLATED_CODE The error code for Ill-formed model.
static int	RANGE_EXCEPTION_CODE The error code for integer range exception.
static int	UNCAUGHT_EXCEPTION_CODE The error code for uncaught exception.

Method Summary

boolean	backtrack() Backtracks and executes the next unexecuted transformation sibling (if any).
IState	createInitialState() Creates the initial state.
void	doTransition(int threadDesc, Transformation t, Action a) Executes a transformation.
void	error(int errCode) Signal an error has been found.
ArrayList<IBacktrackingInfo>	getBacktrackingInfos() Gets the list of backtacking information from the initial state to the current state (last completed transformation).
int	getErrorCount() Gets the number of errors found in the model so far.
IState	getState() Gets the current state.
void	initialize() Perform all work preceding the a call to search().
void	search() Starts the search.
boolean	shouldStore() Determines whether the current state should be stored in the seen before set.
boolean	step() Executes an enabled transformation (if any).
boolean	stepBackward() Backtracks to just before the beginning of the most recent transition executed.
boolean	store() Stores the current state.
void	writeCounterExamples() Externalize all counter-examples found so far.

Methods inherited from interface edu.ksu.cis.projects.bogor.module.IModule

connect, getCopyrightNotice, setOptions

Methods inherited from interface edu.ksu.cis.projects.bogor.util.Disposable

dispose

Field Detail

ILL_FORMED_MODEL_CODE

static final int ILL_FORMED_MODEL_CODE

The error code for ill-formed model.

See Also:

Constant Field Values

INVALID_END_STATE_CODE

static final int INVALID_END_STATE_CODE

The error code for invalid end state.

See Also:

Constant Field Values

ASSERTION_FAILED_CODE

static final int ASSERTION_FAILED_CODE

The error code for assertion failure.

See Also:

Constant Field Values

UNCAUGHT_EXCEPTION_CODE

static final int UNCAUGHT_EXCEPTION_CODE

The error code for uncaught exception.

See Also:

Constant Field Values

RANGE_EXCEPTION_CODE

static final int RANGE_EXCEPTION_CODE

The error code for integer range exception.

See Also:

Constant Field Values

EXT_FAILED_CODE

static final int EXT_FAILED_CODE

The error code for extension failure.

See Also:

Constant Field Values

INVARIANT_VIOLATED_CODE

static final int INVARIANT_VIOLATED_CODE

The error code for Ill-formed model.

See Also:

Constant Field Values

Method Detail

getBacktrackingInfos

ArrayList<IBacktrackingInfo> getBacktrackingInfos()

Gets the list of backtacking information from the initial state to the current state (last completed transformation). The backtracking information is ordered from the first transformation's info to the last transformation's info.

Returns:

The list of backtracking information from the initial state to the current state. Non-null.

getErrorCount

int getErrorCount()

Gets the number of errors found in the model so far.

Returns:

The number errors found in the model so far.

getState

IState getState()

Gets the current state.

Returns:

The current state. Non-null.

backtrack

boolean backtrack()

Backtracks and executes the next unexecuted transformation sibling (if any).

Returns:

True, if there is such a transformation sibling. False, otherwise.

createInitialState

IState createInitialState()

Creates the initial state.

Returns:

The initial state. Non-null.

doTransition

void doTransition(int threadDesc,
                  Transformation t,
                  Action a)

Executes a transformation. If the action is specified, then execute starting from that action.

Parameters:

threadDesc - The thread descriptor that executes the transformation. Must be an active thread descriptor at the current state.

t - The transformation to be executed. Non-null.

a - The action to start from. Must be null if t is not an instance of BlockTransformation. If it is non-null, it indicates the execution starts from the action a.

error

void error(int errCode)

Signal an error has been found.

Parameters:

errCode - The error code.

initialize

void initialize()

Perform all work preceding the a call to search().

search

void search()

Starts the search.

shouldStore

boolean shouldStore()

Determines whether the current state should be stored in the seen before set.

Returns:

True, if it should be stored. False, otherwise.

step

boolean step()

Executes an enabled transformation (if any).

Returns:

True, if an enabled transformation is executed. False, otherwise.

stepBackward

boolean stepBackward()

Backtracks to just before the beginning of the most recent transition executed. Scheduling information accumulated is not reversed. That is, calling step() and stepBackward() successively is not guaranteed to be reflexive.

Returns:

True, if any actions existed to be reversed. False, if the state was in its initial condition.

store

boolean store()

Stores the current state.

Returns:

True, if the state has been seen before. False, otherwise.

writeCounterExamples

void writeCounterExamples()

Externalize all counter-examples found so far.