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

All Superinterfaces:

Disposable, IEventProvider, IModule, IStateEventProvider

All Known Implementing Classes:

DefaultStateFactory

public interface IStateFactory
extends IModule, IStateEventProvider

A state factory interface.

Version:

CVS $Revision: 1.8 $ $Date: 2004/11/06 00:19:50 $

Author:

Robby

Field Summary

static int	EPSILON_THREAD
static String	STATE_AUGMENTER_ID

Method Summary

void	augmentState(IState state, BitBuffer bb) Write extra components of state space into bitwise representation.
IState	createState(IStateFactoryArguments sfa) Creates an initial state.
IStateAugmenter[]	getStateAugmenters() Get the set of state augmenters that contribute to the state space.
int	getThreadDescriptorSeed() Gets the thread descriptor seed.
int	newThreadDescriptor() Creates a fresh thread descriptor.
void	setThreadDescriptorSeed(int newSeed) Sets the thread descriptor seed.
void	validate(IState state) Validates a state.

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

Methods inherited from interface edu.ksu.cis.projects.bogor.module.state.event.IStateEventProvider

getNotifier, getNotifier

Methods inherited from interface edu.ksu.cis.projects.bogor.module.event.IEventProvider

backward, forward, getState, getThreadId, isBackward, isForward, removeContext, setContext

Field Detail

EPSILON_THREAD

static final int EPSILON_THREAD

See Also:

Constant Field Values

STATE_AUGMENTER_ID

static final String STATE_AUGMENTER_ID

See Also:

Constant Field Values

Method Detail

setThreadDescriptorSeed

void setThreadDescriptorSeed(int newSeed)

Sets the thread descriptor seed.

Parameters:

newSeed - The new thread descriptor.

getThreadDescriptorSeed

int getThreadDescriptorSeed()

Gets the thread descriptor seed.

Returns:

The thread descriptor seed.

createState

IState createState(IStateFactoryArguments sfa)

Creates an initial state.

Returns:

The initial state that has one thread, which is the main thread. The main thread is runnable. The lock count of the main thread is zero.

newThreadDescriptor

int newThreadDescriptor()

Creates a fresh thread descriptor.

Returns:

A unique thread descriptor.

validate

void validate(IState state)

Validates a state.

Parameters:

state - The state to be validated. Must be non-null.

getStateAugmenters

IStateAugmenter[] getStateAugmenters()

Get the set of state augmenters that contribute to the state space.

augmentState

void augmentState(IState state,
                  BitBuffer bb)

Write extra components of state space into bitwise representation.