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

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

All Implemented Interfaces:

ISelfDescribingModule, IModule, ISchedulingStrategist, Disposable

public class DefaultSchedulingStrategist
extends Object
implements ISchedulingStrategist, ISelfDescribingModule

Version:

CVS $Revision: 1.26 $ $Date: 2005/06/03 17:11:02 $

Author:

Robby

Nested Class Summary

protected class	DefaultSchedulingStrategist.DefaultSchedulerStrategyInfo
protected class	DefaultSchedulingStrategist.NodeContext

Field Summary

protected DefaultSchedulingStrategist.DefaultSchedulerStrategyInfo	currentDSSI Tracks which nondeterministic branches have been taken inside a single action node.
protected int	currentIndex Points to the index of the current info record used inside currentDSSI.
protected Node	currentNode Stateful variable
protected DefaultSchedulingStrategist.NodeContext	ec Stateful variable
protected IExpEvaluator	ee Runtime module connection
protected String	EXCEPTION_WHEN_FAILED_ID
protected boolean	exceptionWhenFailed Configuration option
protected String	FALSE_WHEN_FAILED_ID
protected boolean	falseWhenFailed Configuration option
protected boolean	interleavingSuppressed Stateful variable
protected HashMap<DefaultSchedulingStrategist.NodeContext,DefaultSchedulingStrategist.DefaultSchedulerStrategyInfo>	nodeDSSIMap Stateful variable
protected int	numNonScriptedScopes Counter giving how many re-entrant levels of non-scripting we're in (used to record whether a counterexample-trail scheduling info is generated).
protected ISearcher	sr Runtime module connection
protected ISchedulingStrategist	ss Runtime module connection
protected SymbolTable	symbolTable Runtime module connection
protected LongIntTable	transformationChooseMap Stateful variable
protected String[]	transformationFilterClassNames Java class names of the custom transformation filters.
protected ITransformationFilter[]	transformationFilters An ordered series of filters which strip out transitions that are otherwise enabled.
protected String	TRUE_WHEN_FAILED_ID
protected boolean	trueWhenFailed Configuration option
protected IValueFactory	vf Runtime module connection

Fields inherited from interface edu.ksu.cis.projects.bogor.module.ISchedulingStrategist

TRANSFORMATION_FILTER_ID

Constructor Summary

DefaultSchedulingStrategist()

Method Summary

int	advise(int extDesc, Node node, IValue[] choices, ISchedulingStrategyInfo ssi) Choose among several possible values for an expression.
int	advise(ISchedulingStrategyContext ssc, int[] threadIds, Transformation[] transformations, ISchedulingStrategyInfo ssi) Choose among several enabled transformations at the beginning of a step.
int	advise(ISchedulingStrategyContext ssc, Transformation[] transformations, ISchedulingStrategyInfo ssi) Choose among non-deterministic transformations to take immediately following the control of transfer from one FSM location to another.
IMessageStore	connect(IBogorConfiguration bc) Connects this modules to other modules.
protected ISchedulingStrategyContext	createContext(int stateId, int invisibleMoves, int threadId, IState state)
void	disableInterleaving() Re-enable the normal calculation of getEnabledTransformation result sets.
void	dispose() Remove references.
void	enableInterleaving() Prevent getEnabledTransformations (all varieties) from stripping out transitions from all threads except the one which most recently moved.
void	enter(ISchedulingStrategyContext ssc, Node node) Notify the scheduler that a thread is entering an FSM.
void	enterSimulation() Inform the scheduling strategist that a series of transitions are about to be executed which should not be pre-scripted (e.g., will not appear in a counterexample trail).
void	exit() Notify the scheduler that a thread is exiting an FSM.
void	exitSimulation() Exit the scope denoted by the corresponding ISchedulingStrategist.enterSimulation() call.
String	getCopyrightNotice() Returns the copyright notice for this module.
IntObjectTable<ArrayList<Transformation>>	getEnabledTransformations(IEnabledTransformationsContext etc) Find all the enabled FSM transitions.
IntObjectTable<ArrayList<Transformation>>	getEnabledTransformations(IEnabledTransformationsContext etc, Set<Transformation> ignoredTransformations) Find all the enabled FSM transitions except those given in ignoredTransformations.
protected FSMSymbolTable	getFSMSymbolTable(IState state, int threadId)
Pair<Domain,Boolean>	getOptionDomain(String id)
Collection<Triple<String,Boolean,OptionScope>>	getOptionIds()
Collection<String>	getSuggestedValues(String id, IBogorConfiguration bc, SymbolTable st)
ITransformationFilter[]	getTransformationFilters() Retrieve the set of transformation filters configured via the ISchedulingStrategist.TRANSFORMATION_FILTER_ID option.
IntObjectTable<ArrayList<Transformation>>	getWorkSet(IEnabledTransformationsContext etc) Find a reduced set of transitions whose executions will suffice to represent the execution of all enabled transformations.
IntObjectTable<ArrayList<Transformation>>	getWorkSet(IEnabledTransformationsContext etc, Set<Transformation> ignoredTransformations) Find a reduced set of transitions whose executions will suffice to represent the execution of all enabled transformations.
boolean	isEnabled(IState state, Transformation t, int threadId) Test if a FSM transition is enabled with respect to a particular thread.
boolean	isInSimulatingScope()
ISchedulingStrategyInfo	newStrategyInfo() Construct a scheduling context information records appropriate to the currently-used schedule module.
protected void	next() Set up the bookkeeping so that each choice point for the current action will point to the next option (compared to last time).
IMessageStore	setOptions(String key, Properties configuration) Sets the options for this module.
boolean	validate(String id, String value, IBogorConfiguration bc, SymbolTable st, Collection<FileMessage> errors) Checks whether the value of a configuration option is legal.

Methods inherited from class java.lang.Object

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

Field Detail

TRUE_WHEN_FAILED_ID

protected String TRUE_WHEN_FAILED_ID

FALSE_WHEN_FAILED_ID

protected String FALSE_WHEN_FAILED_ID

EXCEPTION_WHEN_FAILED_ID

protected String EXCEPTION_WHEN_FAILED_ID

trueWhenFailed

protected boolean trueWhenFailed

Configuration option

falseWhenFailed

protected boolean falseWhenFailed

Configuration option

exceptionWhenFailed

protected boolean exceptionWhenFailed

Configuration option

symbolTable

protected SymbolTable symbolTable

Runtime module connection

ss

protected ISchedulingStrategist ss

Runtime module connection

vf

protected IValueFactory vf

Runtime module connection

ee

protected IExpEvaluator ee

Runtime module connection

sr

protected ISearcher sr

Runtime module connection

currentDSSI

protected DefaultSchedulingStrategist.DefaultSchedulerStrategyInfo currentDSSI

Tracks which nondeterministic branches have been taken inside a single action node.

currentIndex

protected int currentIndex

Points to the index of the current info record used inside currentDSSI.

currentNode

protected Node currentNode

Stateful variable

ec

protected DefaultSchedulingStrategist.NodeContext ec

Stateful variable

nodeDSSIMap

protected HashMap<DefaultSchedulingStrategist.NodeContext,DefaultSchedulingStrategist.DefaultSchedulerStrategyInfo> nodeDSSIMap

Stateful variable

transformationChooseMap

protected LongIntTable transformationChooseMap

Stateful variable

interleavingSuppressed

protected boolean interleavingSuppressed

Stateful variable

transformationFilterClassNames

protected String[] transformationFilterClassNames

Java class names of the custom transformation filters.

numNonScriptedScopes

protected int numNonScriptedScopes

Counter giving how many re-entrant levels of non-scripting we're in (used to record whether a counterexample-trail scheduling info is generated).

transformationFilters

protected ITransformationFilter[] transformationFilters

An ordered series of filters which strip out transitions that are otherwise enabled.

Constructor Detail

DefaultSchedulingStrategist

public DefaultSchedulingStrategist()

Method Detail

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.

enterSimulation

public void enterSimulation()

Description copied from interface: ISchedulingStrategist

Inform the scheduling strategist that a series of transitions are about to be executed which should not be pre-scripted (e.g., will not appear in a counterexample trail). Re-entrance is allowed here.

Specified by:

enterSimulation in interface ISchedulingStrategist

exitSimulation

public void exitSimulation()

Description copied from interface: ISchedulingStrategist

Exit the scope denoted by the corresponding ISchedulingStrategist.enterSimulation() call.

Specified by:

exitSimulation in interface ISchedulingStrategist

isInSimulatingScope

public boolean isInSimulatingScope()

Specified by:

isInSimulatingScope in interface ISchedulingStrategist

disableInterleaving

public void disableInterleaving()

Description copied from interface: ISchedulingStrategist

Re-enable the normal calculation of getEnabledTransformation result sets. See the comments for ISchedulingStrategist.enableInterleaving() for more details.

Specified by:

disableInterleaving in interface ISchedulingStrategist

enableInterleaving

public void enableInterleaving()

Description copied from interface: ISchedulingStrategist

Prevent getEnabledTransformations (all varieties) from stripping out transitions from all threads except the one which most recently moved. The machinery affects by calling this method is structured in a way that calling enableInterleaving in the initial state (that is, before any thread has yet moved) will still allow a thread to be selected and run.

Specified by:

enableInterleaving in interface ISchedulingStrategist

isEnabled

public boolean isEnabled(IState state,
                         Transformation t,
                         int threadId)

Description copied from interface: ISchedulingStrategist

Test if a FSM transition is enabled with respect to a particular thread.

Specified by:

isEnabled in interface ISchedulingStrategist

getEnabledTransformations

public IntObjectTable<ArrayList<Transformation>> getEnabledTransformations(IEnabledTransformationsContext etc)

Description copied from interface: ISchedulingStrategist

Find all the enabled FSM transitions.

Specified by:

getEnabledTransformations in interface ISchedulingStrategist

Returns:

a mapping from thread descriptor (int) to an ArrayList<Transformation> of the transformations enabled for that thread.

getEnabledTransformations

public IntObjectTable<ArrayList<Transformation>> getEnabledTransformations(IEnabledTransformationsContext etc,
                                                                           Set<Transformation> ignoredTransformations)

Description copied from interface: ISchedulingStrategist

Find all the enabled FSM transitions except those given in ignoredTransformations.

Specified by:

getEnabledTransformations in interface ISchedulingStrategist

ignoredTransformations - a Set<Transformation> of transformations to ignore across all threads

Returns:

a mapping from thread descriptor (int) to an ArrayList<Transformation> of the transformations enabled for that thread.

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.

getWorkSet

public IntObjectTable<ArrayList<Transformation>> getWorkSet(IEnabledTransformationsContext etc,
                                                            Set<Transformation> ignoredTransformations)

Description copied from interface: ISchedulingStrategist

Find a reduced set of transitions whose executions will suffice to represent the execution of all enabled transformations.

Specified by:

getWorkSet in interface ISchedulingStrategist

ignoredTransformations - a Set<Transformation> of transformations to ignore across all threads

Returns:

a mapping from thread descriptor (int) to an ArrayList<Transformation> of the transformations enabled for that thread.

getWorkSet

public IntObjectTable<ArrayList<Transformation>> getWorkSet(IEnabledTransformationsContext etc)

Description copied from interface: ISchedulingStrategist

Find a reduced set of transitions whose executions will suffice to represent the execution of all enabled transformations.

Specified by:

getWorkSet in interface ISchedulingStrategist

Returns:

a mapping from thread descriptor (int) to an ArrayList<Transformation> of the transformations enabled for that thread.

getTransformationFilters

public ITransformationFilter[] getTransformationFilters()

Description copied from interface: ISchedulingStrategist

Retrieve the set of transformation filters configured via the ISchedulingStrategist.TRANSFORMATION_FILTER_ID option.

Specified by:

getTransformationFilters in interface ISchedulingStrategist

advise

public int advise(ISchedulingStrategyContext ssc,
                  Transformation[] transformations,
                  ISchedulingStrategyInfo ssi)

Description copied from interface: ISchedulingStrategist

Choose among non-deterministic transformations to take immediately following the control of transfer from one FSM location to another. This should be the very last thing done in a step.

Specified by:

advise in interface ISchedulingStrategist

Returns:

advise

public int advise(ISchedulingStrategyContext ssc,
                  int[] threadIds,
                  Transformation[] transformations,
                  ISchedulingStrategyInfo ssi)

Description copied from interface: ISchedulingStrategist

Choose among several enabled transformations at the beginning of a step.

Specified by:

advise in interface ISchedulingStrategist

Returns:

advise

public int advise(int extDesc,
                  Node node,
                  IValue[] choices,
                  ISchedulingStrategyInfo ssi)

Description copied from interface: ISchedulingStrategist

Choose among several possible values for an expression. This may be done in the "middle" of a step: after selection of the Transformation to execute and before the selection of an optional post-control-transfer metadata Transformation (e.g., for property- checking automata).

Specified by:

advise in interface ISchedulingStrategist

Returns:

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.

dispose

public void dispose()

Description copied from interface: Disposable

Remove references. Once called, avoid using this object.

Specified by:

dispose in interface Disposable

enter

public void enter(ISchedulingStrategyContext ssc,
                  Node node)

Description copied from interface: ISchedulingStrategist

Notify the scheduler that a thread is entering an FSM.

Specified by:

enter in interface ISchedulingStrategist

exit

public void exit()

Description copied from interface: ISchedulingStrategist

Notify the scheduler that a thread is exiting an FSM.

Specified by:

exit in interface ISchedulingStrategist

newStrategyInfo

public ISchedulingStrategyInfo newStrategyInfo()

Description copied from interface: ISchedulingStrategist

Construct a scheduling context information records appropriate to the currently-used schedule module. The class used is normally private to the specific implementation of ISchedulingStrategist.

Specified by:

newStrategyInfo in interface ISchedulingStrategist

Returns:

getFSMSymbolTable

protected FSMSymbolTable getFSMSymbolTable(IState state,
                                           int threadId)

createContext

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

next

protected void next()

Set up the bookkeeping so that each choice point for the current action will point to the next option (compared to last time).

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