edu.ksu.cis.projects.bogor.module
Class DefaultSearcher

java.lang.Object
  edu.ksu.cis.projects.bogor.module.DefaultSearcher

All Implemented Interfaces:

ISelfDescribingModule, IModule, ISearcher, Disposable

public class DefaultSearcher
extends Object
implements ISearcher, ISelfDescribingModule

Version:

CVS $Revision: 1.74 $ $Date: 2005/06/08 03:06:16 $

Author:

Robby , Matt Hoosier

Nested Class Summary

protected class	DefaultSearcher.FoundValueException
protected class	DefaultSearcher.MaxErrorReachedException

Field Summary

protected static String	ALL_AS_ERRORS_ID
protected boolean	allAsErrors
protected IActionTaker	at
protected ArrayList<IBacktrackingInfo>	backtrackingInfos
protected IBogorConfiguration	bc
protected IBacktrackingInfoFactory	bif
protected ICounterExampleWriter	cew
protected static String	CHECK_BACKTRACK_ID
protected boolean	checkBacktrack
protected int	currentDepth
protected int	currentMaxDepth
protected IExpEvaluator	ee
protected int	errors
protected String[]	invariants
protected static String	INVARIANTS_ID
protected int	invisibleMoves
protected boolean	isInvisible
protected int	lastMovedThreadId
protected int	lastUpdatedStates
protected long	lastUpdatedTransitions
protected static String	MAX_DEPTH_ID
protected static String	MAX_ERRORS_ID
protected static String	MAX_INVISIBLE_MOVES_ID
protected int	maxDepth
protected int	maxErrors
protected int	maxInvisibleMoves
protected IProgressManager	pm
protected static String	PRINT_COUNTER_EXAMPLES_ID
protected static String	PRINT_STATUS_ID
protected static String	PRINT_VERBOSE_TRACE_ID
protected boolean	printCounterExamples
protected boolean	printStatus
protected boolean	printVerboseTrace
protected PrintWriter	pw
protected boolean	seenState
protected int	seenStates
protected IStateFactory	sf
protected IStateManager	sm
protected ISearcher	sr
protected ISchedulingStrategist	ss
protected long	startTime
protected IState	state
protected int	stateId
protected SymbolTable	symbolTable
protected ITransformer	tr
protected static String	TRAIL_EXT
protected long	transitions
protected static String	UPDATE_STATE_INCREMENT_ID
protected static String	UPDATE_TRANSITION_INCREMENT_ID
protected int	updateStateIncrement
protected long	updateTransitionIncrement
protected IValueFactory	vf
protected static String	WRITE_TRAIL_FILE_ID
protected boolean	writeTrailFile

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

DefaultSearcher()

Method Summary

protected void	addAll(ArrayList<IBacktrackingInfo> result, IBacktrackingInfo[] bis)
boolean	backtrack() Backtracks and executes the next unexecuted transformation sibling (if any).
protected IBacktrackingInfo	backtrack(IState state, ArrayList<IBacktrackingInfo> backtrackingInfos)
protected IBacktrackingInfo	backtrackToTransitionBeginning(IState state, ArrayList<IBacktrackingInfo> backtrackingInfos) Rolls back the state to the moment just before the most recent transition.
protected void	checkExceptions()
protected boolean	checkInvariants()
IMessageStore	connect(IBogorConfiguration bc) Connects this modules to other modules.
protected ISchedulingStrategyContext	createContext(int stateId, int invisibleMoves, int threadId, IState state)
protected IEnabledTransformationsContext	createContext(IState state, int stateId, int invisibleMoves, int[] threadIds)
IState	createInitialState() Creates the initial state.
void	dispose() Remove references.
protected void	doPostTransformationBookkeeping(int lastMovedThreadId, ISchedulingStrategyInfo ssi)
void	doTransition(int threadId, Transformation t, Action a) Executes a transformation.
protected void	doTransition(ISchedulingStrategyContext ssc, Transformation t, Action a)
protected void	dumpBacktrackingStack(PrintWriter pw, ArrayList<IBacktrackingInfo> backtrackingInfos)
void	error(int errCode) Signal an error has been found.
protected ArrayList<ICounterExampleSchedulingInfo>	extractErrorSchedule(ArrayList<IBacktrackingInfo> backtrackingInfos)
protected void	fillInitialVariableValues(IState vanillaState, IStateFactoryArguments args)
protected ITransformationsBacktrackingInfo	findMostRecentTransformationBacktrackingInfo()
ArrayList<IBacktrackingInfo>	getBacktrackingInfos() Gets the list of backtacking information from the initial state to the current state (last completed transformation).
String	getCopyrightNotice() Returns the copyright notice for this module.
int	getErrorCount() Gets the number of errors found in the model so far.
protected FSMSymbolTable	getFSMSymbolTable(int locDesc)
protected FSMSymbolTable	getFSMSymbolTable(IState state, int threadId)
protected IStateFactoryArguments	getInitialStateFactoryArguments()
protected Location	getLocation(int locDesc)
protected Location	getLocation(IState state, int threadId)
protected String	getMemory(long mem)
Pair<Domain,Boolean>	getOptionDomain(String id)
Collection<Triple<String,Boolean,OptionScope>>	getOptionIds()
IState	getState() Gets the current state.
Collection<String>	getSuggestedValues(String id, IBogorConfiguration bc, SymbolTable st)
protected String	getTime(long time)
void	initialize() Perform all work preceding the a call to search().
protected void	makeChoices(IntObjectTable<ArrayList<Transformation>> ets, int[] threadIds, Transformation[] transformations)
void	search() Starts the search.
IMessageStore	setOptions(String key, Properties configuration) Sets the options for this module.
protected boolean	shouldActivateThread(FSM fsm)
protected boolean	shouldBacktrack()
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.
protected void	storeCounterExample(ArrayList<IBacktrackingInfo> backtrackingInfos, int stateId, int invisibleMoves, String reason)
boolean	validate(String id, String value, IBogorConfiguration bc, SymbolTable st, Collection<FileMessage> errors) Checks whether the value of a configuration option is legal.
void	writeCounterExamples() Externalize all counter-examples found so far.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

PRINT_VERBOSE_TRACE_ID

protected static final String PRINT_VERBOSE_TRACE_ID

See Also:

Constant Field Values

PRINT_STATUS_ID

protected static final String PRINT_STATUS_ID

See Also:

Constant Field Values

TRAIL_EXT

protected static final String TRAIL_EXT

See Also:

Constant Field Values

PRINT_COUNTER_EXAMPLES_ID

protected static final String PRINT_COUNTER_EXAMPLES_ID

See Also:

Constant Field Values

WRITE_TRAIL_FILE_ID

protected static final String WRITE_TRAIL_FILE_ID

See Also:

Constant Field Values

ALL_AS_ERRORS_ID

protected static final String ALL_AS_ERRORS_ID

See Also:

Constant Field Values

MAX_ERRORS_ID

protected static final String MAX_ERRORS_ID

See Also:

Constant Field Values

MAX_DEPTH_ID

protected static final String MAX_DEPTH_ID

See Also:

Constant Field Values

MAX_INVISIBLE_MOVES_ID

protected static final String MAX_INVISIBLE_MOVES_ID

See Also:

Constant Field Values

UPDATE_STATE_INCREMENT_ID

protected static final String UPDATE_STATE_INCREMENT_ID

See Also:

Constant Field Values

UPDATE_TRANSITION_INCREMENT_ID

protected static final String UPDATE_TRANSITION_INCREMENT_ID

See Also:

Constant Field Values

INVARIANTS_ID

protected static final String INVARIANTS_ID

See Also:

Constant Field Values

CHECK_BACKTRACK_ID

protected static final String CHECK_BACKTRACK_ID

See Also:

Constant Field Values

printCounterExamples

protected boolean printCounterExamples

writeTrailFile

protected boolean writeTrailFile

allAsErrors

protected boolean allAsErrors

printVerboseTrace

protected boolean printVerboseTrace

printStatus

protected boolean printStatus

maxErrors

protected int maxErrors

maxDepth

protected int maxDepth

updateStateIncrement

protected int updateStateIncrement

maxInvisibleMoves

protected int maxInvisibleMoves

updateTransitionIncrement

protected long updateTransitionIncrement

checkBacktrack

protected boolean checkBacktrack

invariants

protected String[] invariants

pw

protected PrintWriter pw

backtrackingInfos

protected ArrayList<IBacktrackingInfo> backtrackingInfos

bc

protected IBogorConfiguration bc

at

protected IActionTaker at

bif

protected IBacktrackingInfoFactory bif

cew

protected ICounterExampleWriter cew

ee

protected IExpEvaluator ee

ss

protected ISchedulingStrategist ss

state

protected IState state

sf

protected IStateFactory sf

sm

protected IStateManager sm

sr

protected ISearcher sr

tr

protected ITransformer tr

vf

protected IValueFactory vf

pm

protected IProgressManager pm

symbolTable

protected SymbolTable symbolTable

isInvisible

protected boolean isInvisible

seenState

protected boolean seenState

lastMovedThreadId

protected int lastMovedThreadId

stateId

protected int stateId

invisibleMoves

protected int invisibleMoves

currentDepth

protected int currentDepth

currentMaxDepth

protected int currentMaxDepth

errors

protected int errors

seenStates

protected int seenStates

startTime

protected long startTime

transitions

protected long transitions

lastUpdatedTransitions

protected long lastUpdatedTransitions

lastUpdatedStates

protected int lastUpdatedStates

Constructor Detail

DefaultSearcher

public DefaultSearcher()

Method Detail

getBacktrackingInfos

public ArrayList<IBacktrackingInfo> getBacktrackingInfos()

Description copied from interface: ISearcher

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.

Specified by:

getBacktrackingInfos in interface ISearcher

Returns:

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

getCopyrightNotice

public String getCopyrightNotice()

Description copied from interface: IModule

Returns the copyright notice for this module.

Specified by:

getCopyrightNotice in interface IModule

Returns:

The copyright notice for this module. Returns null if no additional notice is necessary.

getErrorCount

public int getErrorCount()

Description copied from interface: ISearcher

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

Specified by:

getErrorCount in interface ISearcher

Returns:

The number errors found in the model so far.

setOptions

public IMessageStore setOptions(String key,
                                Properties configuration)

Description copied from interface: IModule

Sets the options for this module.

Specified by:

setOptions in interface IModule

Parameters:

key - The key (prefix) for this module options. Must be non-null. The key is used for module specific options.

configuration - The options for all modules. Must be non-null.

getState

public IState getState()

Description copied from interface: ISearcher

Gets the current state.

Specified by:

getState in interface ISearcher

Returns:

The current state. Non-null.

backtrack

public boolean backtrack()

Description copied from interface: ISearcher

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

Specified by:

backtrack in interface ISearcher

Returns:

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

connect

public IMessageStore connect(IBogorConfiguration bc)

Description copied from interface: IModule

Connects this modules to other modules.

Specified by:

connect in interface IModule

Parameters:

bc - The Bogor configuration containing modules to connect to. Must be non-null.

createInitialState

public IState createInitialState()

Description copied from interface: ISearcher

Creates the initial state.

Specified by:

createInitialState in interface ISearcher

Returns:

The initial state. Non-null.

dispose

public void dispose()

Description copied from interface: Disposable

Remove references. Once called, avoid using this object.

Specified by:

dispose in interface Disposable

doTransition

public void doTransition(int threadId,
                         Transformation t,
                         Action a)

Description copied from interface: ISearcher

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

Specified by:

doTransition in interface ISearcher

Parameters:

threadId - 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

public void error(int errCode)

Description copied from interface: ISearcher

Signal an error has been found.

Specified by:

error in interface ISearcher

Parameters:

errCode - The error code.

initialize

public void initialize()

Description copied from interface: ISearcher

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

Specified by:

initialize in interface ISearcher

search

public void search()

Description copied from interface: ISearcher

Starts the search.

Specified by:

search in interface ISearcher

shouldStore

public boolean shouldStore()

Description copied from interface: ISearcher

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

Specified by:

shouldStore in interface ISearcher

Returns:

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

step

public boolean step()

Description copied from interface: ISearcher

Executes an enabled transformation (if any).

Specified by:

step in interface ISearcher

Returns:

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

stepBackward

public boolean stepBackward()

Description copied from interface: ISearcher

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.

Specified by:

stepBackward in interface ISearcher

Returns:

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

store

public boolean store()

Description copied from interface: ISearcher

Stores the current state.

Specified by:

store in interface ISearcher

Returns:

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

writeCounterExamples

public void writeCounterExamples()

Description copied from interface: ISearcher

Externalize all counter-examples found so far.

Specified by:

writeCounterExamples in interface ISearcher

getFSMSymbolTable

protected FSMSymbolTable getFSMSymbolTable(int locDesc)

getFSMSymbolTable

protected FSMSymbolTable getFSMSymbolTable(IState state,
                                           int threadId)

getInitialStateFactoryArguments

protected IStateFactoryArguments getInitialStateFactoryArguments()

getLocation

protected Location getLocation(IState state,
                               int threadId)

getLocation

protected Location getLocation(int locDesc)

getMemory

protected String getMemory(long mem)

getTime

protected String getTime(long time)

addAll

protected void addAll(ArrayList<IBacktrackingInfo> result,
                      IBacktrackingInfo[] bis)

backtrack

protected IBacktrackingInfo backtrack(IState state,
                                      ArrayList<IBacktrackingInfo> backtrackingInfos)

backtrackToTransitionBeginning

protected IBacktrackingInfo backtrackToTransitionBeginning(IState state,
                                                           ArrayList<IBacktrackingInfo> backtrackingInfos)

Rolls back the state to the moment just before the most recent transition.

Parameters:

state - system state to revert

backtrackingInfos - stack of reverse deltas to roll back state

Returns:

the ITransformationsBacktrackingInfo of the most recent transition (incomplete)

checkExceptions

protected void checkExceptions()

checkInvariants

protected boolean checkInvariants()

createContext

protected ISchedulingStrategyContext createContext(int stateId,
                                                   int invisibleMoves,
                                                   int threadId,
                                                   IState state)

createContext

protected IEnabledTransformationsContext createContext(IState state,
                                                       int stateId,
                                                       int invisibleMoves,
                                                       int[] threadIds)

doPostTransformationBookkeeping

protected void doPostTransformationBookkeeping(int lastMovedThreadId,
                                               ISchedulingStrategyInfo ssi)

doTransition

protected void doTransition(ISchedulingStrategyContext ssc,
                            Transformation t,
                            Action a)

dumpBacktrackingStack

protected void dumpBacktrackingStack(PrintWriter pw,
                                     ArrayList<IBacktrackingInfo> backtrackingInfos)

extractErrorSchedule

protected ArrayList<ICounterExampleSchedulingInfo> extractErrorSchedule(ArrayList<IBacktrackingInfo> backtrackingInfos)

findMostRecentTransformationBacktrackingInfo

protected ITransformationsBacktrackingInfo findMostRecentTransformationBacktrackingInfo()

fillInitialVariableValues

protected void fillInitialVariableValues(IState vanillaState,
                                         IStateFactoryArguments args)

makeChoices

protected void makeChoices(IntObjectTable<ArrayList<Transformation>> ets,
                           int[] threadIds,
                           Transformation[] transformations)

shouldActivateThread

protected boolean shouldActivateThread(FSM fsm)

shouldBacktrack

protected boolean shouldBacktrack()

storeCounterExample

protected void storeCounterExample(ArrayList<IBacktrackingInfo> backtrackingInfos,
                                   int stateId,
                                   int invisibleMoves,
                                   String reason)

getOptionIds

public Collection<Triple<String,Boolean,OptionScope>> getOptionIds()

Specified by:

getOptionIds in interface ISelfDescribingModule

Returns:

a set of tuples whose first element says the name of the option, and whose second element says whether the option is required, and whose third element says whether the option is private to this module (and thus prefixed by the interface implemented, e.g., edu.ksu.cis.projects.bogor.module.ISearcher) or global in scope (and thus no qualifier is prepended).

getOptionDomain

public Pair<Domain,Boolean> getOptionDomain(String id)

Specified by:

getOptionDomain in interface ISelfDescribingModule

Returns:

a tuple whose first element says the domain of the option values, and whose second element says whether the option is multivalued (that is, a comma-separated list)

getSuggestedValues

public Collection<String> getSuggestedValues(String id,
                                             IBogorConfiguration bc,
                                             SymbolTable st)

Specified by:

getSuggestedValues in interface ISelfDescribingModule

validate

public boolean validate(String id,
                        String value,
                        IBogorConfiguration bc,
                        SymbolTable st,
                        Collection<FileMessage> errors)

Checks whether the value of a configuration option is legal.

Specified by:

validate in interface ISelfDescribingModule

Parameters:

id - the option's name, as returned by the first tuple element of an item returned by getOptionIds()

value - the value of the option, or null if unconfigued

st - the symbol table for the BIR model

errors - a container into which errors should be put. Implementors should not assume that errors is empty upon entry into this method; it may aggregate the results of calling validate on many ISelfDescribingModule instances.

Returns:

true iff the option is supported and its value is legal