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

All Superinterfaces:
Disposable, IModule
All Known Implementing Classes:
DefaultCounterExampleWriter.GuidedSchedulingStrategistProxy, DefaultSchedulingStrategist

public interface ISchedulingStrategist
extends IModule

Main scheduler module for Bogor.

Version:
CVS $Revision: 1.10 $ $Date: 2005/06/03 17:11:02 $
Author:
Robby , Matt Hoosier

Field Summary
static String TRANSFORMATION_FILTER_ID
          Configuration option to give an order list of classnames which implement ITransformationFilter to provide domain-customized removal of infeasible transformations.
 
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.
 void disableInterleaving()
          Re-enable the normal calculation of getEnabledTransformation result sets.
 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 enterSimulation() call.
 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.
 ITransformationFilter[] getTransformationFilters()
          Retrieve the set of transformation filters configured via the 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.
 
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

TRANSFORMATION_FILTER_ID

static final String TRANSFORMATION_FILTER_ID
Configuration option to give an order list of classnames which implement ITransformationFilter to provide domain-customized removal of infeasible transformations.

See Also:
Constant Field Values
Method Detail

enterSimulation

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). Re-entrance is allowed here.


exitSimulation

void exitSimulation()
Exit the scope denoted by the corresponding enterSimulation() call.


isInSimulatingScope

boolean isInSimulatingScope()

enableInterleaving

void enableInterleaving()
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.


disableInterleaving

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


isEnabled

boolean isEnabled(IState state,
                  Transformation t,
                  int threadId)
Test if a FSM transition is enabled with respect to a particular thread.


getEnabledTransformations

IntObjectTable<ArrayList<Transformation>> getEnabledTransformations(IEnabledTransformationsContext etc)
Find all the enabled FSM transitions.

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

getEnabledTransformations

IntObjectTable<ArrayList<Transformation>> getEnabledTransformations(IEnabledTransformationsContext etc,
                                                                    Set<Transformation> ignoredTransformations)
Find all the enabled FSM transitions except those given in ignoredTransformations.

Parameters:
etc -
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

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.

Parameters:
etc -
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

IntObjectTable<ArrayList<Transformation>> getWorkSet(IEnabledTransformationsContext etc)
Find a reduced set of transitions whose executions will suffice to represent the execution of all enabled transformations.

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

getTransformationFilters

ITransformationFilter[] getTransformationFilters()
Retrieve the set of transformation filters configured via the TRANSFORMATION_FILTER_ID option.


advise

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. This should be the very last thing done in a step.

Parameters:
ssc -
transformations -
ssi -
Returns:

advise

int advise(ISchedulingStrategyContext ssc,
           int[] threadIds,
           Transformation[] transformations,
           ISchedulingStrategyInfo ssi)
Choose among several enabled transformations at the beginning of a step.

Parameters:
ssc -
threadIds -
transformations -
ssi -
Returns:

advise

int advise(int extDesc,
           Node node,
           IValue[] choices,
           ISchedulingStrategyInfo ssi)
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).

Parameters:
extDesc -
node -
choices -
ssi -
Returns:

enter

void enter(ISchedulingStrategyContext ssc,
           Node node)
Notify the scheduler that a thread is entering an FSM.

Parameters:
ssc -
node -

exit

void exit()
Notify the scheduler that a thread is exiting an FSM.


newStrategyInfo

ISchedulingStrategyInfo newStrategyInfo()
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.

Returns: