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

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

All Implemented Interfaces:

StateEngine.EntryStack

Enclosing class:

StateEngine

public final class StateEngine.EntryStackLazy

extends Object

implements StateEngine.EntryStack

Path storage mechanism. Disposes of popped states as late as possible (i.e. only when another push is performed,) so suitable for use by model checkers. INTERNAL USE ONLY

See Also:

StateEngine.LAZY_POP

Method Summary

void	advancePastEnd() Restore the trace to the failure point.
int	getMark() Get the current mark.
StateEngine.StackEntry	index(int index) Peek at the state at the given depth.
int	maxdepth() What is the maximum size of the stack?
StateEngine.StackEntry	pop() Pop a state off the stack.
Integer	present(StateEngine.MajorState major) Test for the presence of a state.
void	push(StateEngine.StackEntry se) Push a state onto the stack.
void	setRetainLevel(int level) Set the state serialization point.
int	size() How big is the stack?
StateEngine.StackEntry	top() Peek at the top-most state.

Methods inherited from class java.lang.Object

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

Method Detail

push

public void push(StateEngine.StackEntry se)

Description copied from interface: StateEngine.EntryStack

Push a state onto the stack. The state is encoded as a stack entry.

Specified by:

push in interface StateEngine.EntryStack

pop

public StateEngine.StackEntry pop()

Description copied from interface: StateEngine.EntryStack

Pop a state off the stack.

Specified by:

pop in interface StateEngine.EntryStack

present

public Integer present(StateEngine.MajorState major)

Description copied from interface: StateEngine.EntryStack

Test for the presence of a state.

Specified by:

present in interface StateEngine.EntryStack

Following copied from interface: uk.ac.man.cs.rainbow.deadlock.StateEngine.EntryStack

Returns:

The depth on the stack where the state is present, or null if the state is not present.

top

public StateEngine.StackEntry top()

Description copied from interface: StateEngine.EntryStack

Peek at the top-most state.

Specified by:

top in interface StateEngine.EntryStack

index

public StateEngine.StackEntry index(int index)

Description copied from interface: StateEngine.EntryStack

Peek at the state at the given depth.

Specified by:

index in interface StateEngine.EntryStack

size

public int size()

Description copied from interface: StateEngine.EntryStack

How big is the stack?

Specified by:

size in interface StateEngine.EntryStack

maxdepth

public int maxdepth()

Description copied from interface: StateEngine.EntryStack

What is the maximum size of the stack?

Specified by:

maxdepth in interface StateEngine.EntryStack

getMark

public int getMark()

Description copied from interface: StateEngine.EntryStack

Get the current mark. Used to make backtracks more informative in the lazy case. Probably ought to be replaced by a different interface...

Specified by:

getMark in interface StateEngine.EntryStack

Following copied from interface: uk.ac.man.cs.rainbow.deadlock.StateEngine.EntryStack

See Also:

StateEngine.LAZY_POP

advancePastEnd

public void advancePastEnd()
                    throws RainbowException

Description copied from interface: StateEngine.EntryStack

Restore the trace to the failure point. Used to make backtracks more informative in the lazy case. Probably ought to be replaced by a different interface...

Specified by:

advancePastEnd in interface StateEngine.EntryStack

Following copied from interface: uk.ac.man.cs.rainbow.deadlock.StateEngine.EntryStack

See Also:

StateEngine.LAZY_POP

setRetainLevel

public void setRetainLevel(int level)

Description copied from interface: StateEngine.EntryStack

Set the state serialization point.

Specified by:

setRetainLevel in interface StateEngine.EntryStack

Following copied from interface: uk.ac.man.cs.rainbow.deadlock.StateEngine.EntryStack

Parameters:

level - The maximum number of values on the stack to keep hard references to. All the rest are written out to disk to decrease peak memory consumption.

See Also:

ReclaimableSavedState