uk.ac.man.cs.rainbow.simulator
Class StateEnumerator

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.simulator.Scheduler
        |
        +--uk.ac.man.cs.rainbow.simulator.StateEnumerator

All Implemented Interfaces:

Serializable

public class StateEnumerator

extends Scheduler

implements Serializable

Simulation state enumerator. State enumerators are a kind of scheduler that permits precisely controlled execution of a simulation, with an external environment specifiying exactly what action should be performed every time there is a choice. They support state saving and reloading, and can be asked to produce a characterisation of the state of the whole simulation.

See Also:

RainbowThread, Rainbow Implementors Guide, Serialized Form

Inner Class Summary

static class	StateEnumerator.ChanWatch For debugging channel activity.
static class	StateEnumerator.NDData So the state of the scheduler can be characterised.
protected static class	StateEnumerator.SavedEnumeratorState
static class	StateEnumerator.ThreadWatch For debugging thread activity.

Inner classes inherited from class uk.ac.man.cs.rainbow.simulator.Scheduler

Scheduler.ExternalExecutionServer, Scheduler.LabellingAdapter, Scheduler.LabellingListener, Scheduler.ThreadingAdapter, Scheduler.ThreadingListener

Field Summary

static String

DEBUG_COMPILATION_PROPERTY The name of a property to set to true to enable compilation debugging.

Constructor Summary

StateEnumerator()
Create a new state enumerator.

StateEnumerator(File rainbowSourceFile)
Create a new state enumerator with the compiled version of the given file installed.

Method Summary

void	addCodeThread(RASMCode codeBlock) Add a new top-level code thread.
void	advanceTime() Advances time one step.
protected void	asap(RainbowThread thread) Run thread as soon as possible in the current direction.
void	characterise(Data[] vec) Put a characterisation of the state into the given vector.
static boolean	compareCharacterisations(Data[] characterisation1, Data[] characterisation2) Compare two characterisations.
int	countTransitions() Count the transitions out of the current state.
protected boolean	delay(RainbowThread thread, int delay) Delay thread for a bit.
boolean	executeTransition(int transitionIndex) Execute a transition.
int	getCharacterisationLength() How long should a characterisation vector be? For any particular scheduler run, this is fixed, though the value is only determined after initialisation.
long	getTime() What is the current time?
void	initialise() Initialise the scheduler.
boolean	isInitialised() Has this scheduler been initialised yet?
boolean	isNondeterministic() Is the scheduler at a nondeterministic choice point?
void	restoreState(SavedState saved) Reload a saved state.
protected void	reverse(RainbowThread thread) Run thread as soon as possible in the opposite direction.
ReclaimableSavedState	saveState() Save the state for later reloading.
String	toString() What is going on? This is very useful for debugging!

Methods inherited from class uk.ac.man.cs.rainbow.simulator.Scheduler

addLabellingListener, addThreadingListener, readKeyedRegister, readKeyedRegister, removeLabellingListener, removeThreadingListener, setExternalExecutionServer

Methods inherited from class java.lang.Object

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

Field Detail

DEBUG_COMPILATION_PROPERTY

public static final String DEBUG_COMPILATION_PROPERTY

The name of a property to set to true to enable compilation debugging. The value is rainbow.debug.stateenumeratorcompilation.

See Also:

StateEnumerator(File), Boolean.getBoolean(String)

Constructor Detail

StateEnumerator

public StateEnumerator()

Create a new state enumerator.

StateEnumerator

public StateEnumerator(File rainbowSourceFile)
                throws RainbowException,
                       IOException

Create a new state enumerator with the compiled version of the given file installed. Note that you must have the following system properties set up correctly:

• rainbow.stdlib.dir
• rainbow.compiler.class

Parameters:

rainbowSourceFile - The file to load the Rainbow source text from.

Throws:

RainbowException - If something goes wrong during the compilation and linking stages.

IOException - If something goes wrong when reading a source file.

See Also:

RASMCode, Compiler

Method Detail

saveState

public final ReclaimableSavedState saveState()

Save the state for later reloading.

Returns:

Token for use when reloading later. Can only be used in the scheduler object that generated it.

See Also:

restoreState(SavedState)

restoreState

public final void restoreState(SavedState saved)
                        throws RainbowException

Reload a saved state. After reloading, the scheduler will appear to be in exactly the same state as it was prior to the state being saved.

Parameters:

saved - The saved state to reload.

Throws:

RainbowException - If the state was saved by a different scheduler to the one it is being reloaded into.

ReclaimableSavedState.StateReloadException - If a saved state that was moved to disk proves impossible to reload for some reason.

See Also:

saveState()

getCharacterisationLength

public int getCharacterisationLength()

How long should a characterisation vector be? For any particular scheduler run, this is fixed, though the value is only determined after initialisation.

Returns:

The required minimum length of the characterisation vector.

Throws:

java.lang.NullPointerException - If called before the scheduler is initialised.

See Also:

characterise(Data[])

characterise

public void characterise(Data[] vec)

Put a characterisation of the state into the given vector. The characterisation of a simulation is the characterisation of all its threads, combined with the characterisation of the scheduler itself. (The characterisation of the scheduler is simply a description of which thread is undergoing non-deterministic choice.)

Parameters:

vec - The vector to write the characterisation into. The size of this vector is fixed for any simulation run to allow more efficient memory handling.

Throws:

java.lang.NullPointerException - If called before the scheduler is initialised.

java.lang.ArrayIndexOutOfBoundsException - If the given vector is shorter than the required length.

See Also:

getCharacterisationLength(), RainbowThread.characterise()

compareCharacterisations

public static boolean compareCharacterisations(Data[] characterisation1,
                                               Data[] characterisation2)

Compare two characterisations. They are assumed to be characterisations of the same system, and therefore the same length.

Parameters:

characterisation1 - The first characterisation vector to examine.

characterisation2 - The second characterisation vector to examine.

Returns:

Whether the vectors are equal.

addCodeThread

public void addCodeThread(RASMCode codeBlock)

Add a new top-level code thread.

Overrides:

addCodeThread in class Scheduler

Parameters:

codeBlock - The block of code specifying the code to run. The entry point is the first instruction in the block of code.

Throws:

RainbowError - If the scheduler has been initialised.

initialise

public void initialise()
                throws RainbowException

Initialise the scheduler.

Overrides:

initialise in class Scheduler

Throws:

RainbowException - If something goes wrong during initialisation.

See Also:

executeTransition(int)

countTransitions

public int countTransitions()

Count the transitions out of the current state. Note that these transitions might in fact be transitions back into the current state.

Returns:

The number of transitions.

See Also:

executeTransition(int)

executeTransition

public boolean executeTransition(int transitionIndex)
                          throws RainbowException

Execute a transition.

Parameters:

transitionIndex - Which of the possible transitions to execute.

Returns:

If the thread that was the root of the transition became able to be a transition in the target state. When this happens but the characterisation of the state does not change, this can be an indication that a livelock loop is possible in the behaviour of the simulation, meriting special attention by the callee.

Throws:

RainbowError - If the simulation is not initialised, or if the transition index is not in the range 0 to countTransitions().

RainbowException - If something goes wrong during the execution of the transition.

See Also:

initialise(), countTransitions()

advanceTime

public void advanceTime()

Advances time one step. Note that time is not actually a concept that the scheduler uses in deciding what action to perform next, and only serves to aid the user in a trace-back.

See Also:

getTime()

isInitialised

public final boolean isInitialised()

Has this scheduler been initialised yet?

Returns:

Whether the initialise() call has yet been performed.

isNondeterministic

public final boolean isNondeterministic()

Is the scheduler at a nondeterministic choice point?

Returns:

Whether the next executeTransition() will be a performing a choice at a nondeterministic choice point or not.

asap

protected void asap(RainbowThread thread)

Run thread as soon as possible in the current direction.

Overrides:

asap in class Scheduler

Parameters:

thread - The thread to schedule.

reverse

protected void reverse(RainbowThread thread)

Run thread as soon as possible in the opposite direction.

Overrides:

reverse in class Scheduler

Parameters:

thread - The thread to schedule.

delay

protected boolean delay(RainbowThread thread,
                        int delay)

Delay thread for a bit. This is a null-op in this implementation.

Overrides:

delay in class Scheduler

Parameters:

thread - The thread to delay.

delay - How long to delay for.

Returns:

Has the thread been delayed? If not, it should keep on executing.

getTime

public long getTime()

What is the current time?

Overrides:

getTime in class Scheduler

Returns:

The time.

toString

public String toString()

What is going on? This is very useful for debugging!

Overrides:

toString in class Object