uk.ac.man.cs.rainbow.deadlock
Class StateEngine

java.lang.Object
  |
  +--uk.ac.man.cs.rainbow.deadlock.StateEngine

public class StateEngine

extends Object

Rewindable state system enumeration engine.

See Also:

StateEnumerator, DeadlockChecker

Inner Class Summary

static class	StateEngine.AlreadyInitialisedException
static class	StateEngine.ChannelEvent Events that happen on channels during state enumeration.
static class	StateEngine.Debug For debugging.
static interface	StateEngine.EntryStack Path storage mechanism spec.
class	StateEngine.EntryStackEager Path storage mechanism.
class	StateEngine.EntryStackLazy Path storage mechanism.
static class	StateEngine.EntryStore Visited state storage mechanism.
static interface	StateEngine.EventStack A stack of channel events.
class	StateEngine.EventStackEager Stack of channel events.
class	StateEngine.EventStackLazy Stack of channel events.
static class	StateEngine.ExecuteResult Used to indicate what happened during an execute step.
class	StateEngine.Failing Encapsulate state info when falling back from a possible failure state.
class	StateEngine.Listener Channel event recording mechanism.
static class	StateEngine.MajorState Major state.
static class	StateEngine.StackEntry An entry on the stack.

Field Summary

static PrintStream	DEBUGGING Where a trace of debugging actions is printed.
static int	EAGER_POP Indicate that all pops are to be carried out as soon as possible.
static int	LAZY_POP Indicate that all pops are to be carried out as late as possible.

Constructor Summary

StateEngine(StateEnumerator enumerator)
Create a new state enumeration engine with no automata attached.

StateEngine(StateEnumerator enumerator, AutomataState automata)
Create a new state enumeration engine attached to control automata.

StateEngine(StateEnumerator enumerator, AutomataState automata, int popStyle)
Create a new state enumeration engine attached to control automata.

Method Summary

protected Data[]	advanceEpsilons() Advance the system over epsilon steps.
boolean	backtrack() Make the system backtrack.
boolean	backtrack(boolean stateValue) Make the system backtrack.
StateEngine.ExecuteResult	execute() Try to execute a non-empty transition to a new state.
StateEngine.ExecuteResult	execute(boolean resetCounter) Try to execute a non-empty transition to a new state.
long	getActionCount() Report the number of state-changes that have happened.
StateEngine.ChannelEvent[][]	getChannelEvents() Get the events that have happened on labelled channels.
StateEngine.ChannelEvent[][]	getChannelEvents(int index) Get the events that have happened on labelled channels up to the given depth on the current path.
long	getMinorActionCount() Report the number of times the scheduler has been called.
int	getPathLength() Report the length of the current path.
int	getPathMax() Report the maximum length of the path.
SavedState	getState(int index) Get the state at a given depth on the current path.
int	getStateCount() Report the number of distinct states visited.
void	pop() Pop a state from the stack.
void	push() Save the current state and reset the transition index counter to zero.
void	stepPastEnd() Generate extra state to demonstrate unwanted loop.
Boolean	visited() Has the current state has been visited before? This is useful when the state of the automata changes.

Methods inherited from class java.lang.Object

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

Field Detail

DEBUGGING

public static final PrintStream DEBUGGING

Where a trace of debugging actions is printed. null if no such trace is produced at all.

EAGER_POP

public static final int EAGER_POP

Indicate that all pops are to be carried out as soon as possible. This is the default action style, and it is suitable for use with deadlock checkers (or any model checker working with a simple safety property.)

See Also:

StateEngine(StateEnumerator,AutomataState,int)

LAZY_POP

public static final int LAZY_POP

Indicate that all pops are to be carried out as late as possible. This action style is suitable for use with advanced model checkers (particularly those that must backtrack before they can detect a failure of some kind.)

See Also:

StateEngine(StateEnumerator,AutomataState,int)

Constructor Detail

StateEngine

public StateEngine(StateEnumerator enumerator)
            throws RainbowException

Create a new state enumeration engine with no automata attached. This is suitable for deadlock checking. The scheduler should not be initialised, as it gets initialised during the creation of this object.

Parameters:

enumerator - The scheduler that this system will analyse.

Throws:

RainbowException - If the scheduler was initialised, or if something goes wrong during initialisation.

See Also:

DeadlockChecker

StateEngine

public StateEngine(StateEnumerator enumerator,
                   AutomataState automata)
            throws RainbowException

Create a new state enumeration engine attached to control automata. The scheduler should not be initialised as it gets initialised during the creation of this object.

Parameters:

enumerator - The scheduler that this system will analyse.

automata - Reference to the collected state of the automata to attach to.

Throws:

RainbowException - If the scheduler was initialised, or if something goes wrong during initialisation.

StateEngine

public StateEngine(StateEnumerator enumerator,
                   AutomataState automata,
                   int popStyle)
            throws RainbowException

Create a new state enumeration engine attached to control automata. The scheduler should not be initialised as it gets initialised during the creation of this object.

Parameters:

enumerator - The scheduler that this system will analyse.

automata - Reference to the collected state of the automata to attach to.

popStyle - Sets the style of state pop used in the internal stack.

Throws:

StateEngine.AlreadyInitialisedException - If the state enumerator was already initialised.

RainbowException - If something goes wrong during initialisation.

See Also:

EAGER_POP, LAZY_POP

Method Detail

advanceEpsilons

protected Data[] advanceEpsilons()
                          throws RainbowException

Advance the system over epsilon steps. An epsilon step is what occurs when a transition is performed but the characterised state does not change. When there is an infinite loop of epsiloon steps, this also triggers the return of the system state, which gets converted by the calling code into a report of a self-loop.

Returns:

The new characterised state if the system has managed to move into a new state, or null otherwise.

Throws:

RainbowException - If something goes wrong during step execution.

See Also:

StateEnumerator.countTransitions(), StateEnumerator.executeTransition(int), StateEnumerator.characterise(Data[])

execute

public StateEngine.ExecuteResult execute(boolean resetCounter)
                                  throws RainbowException

Try to execute a non-empty transition to a new state. Also handles loops back to the current state.

Parameters:

resetCounter - Whether to reset the local transition counter first.

Returns:

A token that indicates what happened.

Throws:

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

See Also:

advanceEpsilons(), StateEngine.ExecuteResult

execute

public StateEngine.ExecuteResult execute()
                                  throws RainbowException

Try to execute a non-empty transition to a new state. Also handles loops back to the current state.

Returns:

A token that indicates what happened.

Throws:

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

See Also:

advanceEpsilons(), StateEngine.ExecuteResult

push

public void push()

Save the current state and reset the transition index counter to zero. Called after the model checker has undergone certain kinds of internal transition. Only ever safe when matched with a pop.

pop

public void pop()
         throws RainbowException

Pop a state from the stack. Used to undo a push action with which it should be programmatically paired. Does not put the state backtracked out of into the store.

Throws:

RainbowException - If the stack is empty.

backtrack

public boolean backtrack()
                  throws RainbowException

Make the system backtrack.

Returns:

Whether the system was able to backtrack. If it is not able to backtrack then the whole state-space has been searched.

Throws:

RainbowException - If state reloading fails somehow.

backtrack

public boolean backtrack(boolean stateValue)
                  throws RainbowException

Make the system backtrack.

Parameters:

stateValue - What value is associated with this state in the store?

Returns:

Whether the system was able to backtrack. If it is not able to backtrack then the whole state-space has been searched.

Throws:

RainbowException - If state reloading fails somehow.

visited

public Boolean visited()

Has the current state has been visited before? This is useful when the state of the automata changes.

Returns:

null if the state has not been backtracked out of before, and a Boolean that describes the state if the state has been backtracked out of.

getPathLength

public int getPathLength()

Report the length of the current path.

getPathMax

public int getPathMax()

Report the maximum length of the path.

getStateCount

public int getStateCount()

Report the number of distinct states visited. Strictly, only states that have been backtracked out of are included in this count. Add this to the number of states on the current path to get the number of distinct states seen.

getActionCount

public long getActionCount()

Report the number of state-changes that have happened.

See Also:

advanceEpsilons(), execute(), execute(boolean)

getMinorActionCount

public long getMinorActionCount()

Report the number of times the scheduler has been called.

See Also:

advanceEpsilons(), StateEnumerator.executeTransition(int)

getState

public SavedState getState(int index)

Get the state at a given depth on the current path.

Parameters:

index - From where in the current path is the saved state to be returned.

Returns:

A saved state token suitable for reloading into the scheduler passed to the constructor of this class.

Throws:

NullPointerException - If the index is negative or indicates a state off the current path.

See Also:

StateEnumerator.restoreState(SavedState)

getChannelEvents

public StateEngine.ChannelEvent[][] getChannelEvents()

Get the events that have happened on labelled channels.

Returns:

An array of arrays of channel events. Each of the contained arrays contains the events that happened in a particular step.

See Also:

Channel, StateEngine.ChannelEvent, execute()

getChannelEvents

public StateEngine.ChannelEvent[][] getChannelEvents(int index)

Get the events that have happened on labelled channels up to the given depth on the current path.

Parameters:

index - From where in the current path is the channel event vector to be returned.

Returns:

An array of arrays of channel events. Each of the contained arrays contains the events that happened in a particular step.

Throws:

NullPointerException - If the index is negative or indicates a state off the current path.

See Also:

Channel, StateEngine.ChannelEvent, execute()

stepPastEnd

public void stepPastEnd()
                 throws RainbowException

Generate extra state to demonstrate unwanted loop. When you have discovered an unwanted loop (when model checking) you need to run the state engine on one more step from the exact state that lead to the problem so that you can see what the loop actually is.

I have yet to figure out if this has any usefulness to deadlock checking, so the implementation throws an exception there.

Throws:

RainbowException - For many reasons, including if the operation isn't supported with the current stack model.