avrora.stack
Class StateTransitionGraph

java.lang.Object
  avrora.stack.StateTransitionGraph

public class StateTransitionGraph

extends java.lang.Object

Nested Class Summary

static class	StateTransitionGraph.Edge The Edge inner class represents a bidirectional edge between two states.
static class	StateTransitionGraph.EdgeList
static class	StateTransitionGraph.StateInfo The StateInfo class is a representation of both the forward and backward edge list corresponding to a node in the state transition graph.
static class	StateTransitionGraph.StateList

Constructor Summary

StateTransitionGraph(Program p)
The constructor for the StateTransitionGraph class constructs a new state transition graph, with a state cache.

Method Summary

StateTransitionGraph.Edge	addEdge(StateCache.State s, int type, int weight, StateCache.State t) The addEdge() method adds an edge between two states in the state transition graph.
void	addFrontierState(StateCache.State s) The addFrontierState method adds a state to the frontier.
void	deleteStateSets()
void	dump(Printer p)
StateCache.State	getCachedState(MutableState s) The getCachedState() method looks for the a cached, immutable state that corresponds to the given mutable state.
StateCache.State	getEdenState()
long	getEdgeCount()
long	getExploredCount()
long	getFrontierCount()
StateCache.State	getNextFrontierState() The getNextFrontierState() chooses a state off of the state frontier, removes it from the state frontier, and returns it.
StateCache	getStateCache() The getStateCache() method gets the cache of all the states in the state space.
boolean	isExplored(StateCache.State s) The isExplored() method tests whether a given state has been explored before.
boolean	isFrontier(StateCache.State s) The isFrontier() method tests whether a given state is currently in the frontier list of the state transition graph.
StateCache.Set	newSet()
void	setExplored(StateCache.State s) The setExplored() method marks the given state as having been explored.

Methods inherited from class java.lang.Object

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

Constructor Detail

StateTransitionGraph

public StateTransitionGraph(Program p)

The constructor for the StateTransitionGraph class constructs a new state transition graph, with a state cache. The program passed is used as an approximation of the possible size of the state space.

Parameters:

p - the program to create a state transition graph for.

Method Detail

getCachedState

public StateCache.State getCachedState(MutableState s)

The getCachedState() method looks for the a cached, immutable state that corresponds to the given mutable state. If there is no cached state yet, it will create and return a new one.

Parameters:

s - the mutable state to look for

Returns:

an instance of the StateCache.State class

addEdge

public StateTransitionGraph.Edge addEdge(StateCache.State s,
                                         int type,
                                         int weight,
                                         StateCache.State t)

The addEdge() method adds an edge between two states in the state transition graph. The edge has a type and a weight.

Parameters:

s - the source node of the edge

type - the type of the edge as an integer

weight - the weight of the edge as an integer

t - the target node of the edge

getNextFrontierState

public StateCache.State getNextFrontierState()

The getNextFrontierState() chooses a state off of the state frontier, removes it from the state frontier, and returns it. If there are no states left on the state frontier, this method returns null. Note that initially only the eden state is on the frontier.

Returns:

one of the states on the current state frontier; null if there are none.

addFrontierState

public void addFrontierState(StateCache.State s)

The addFrontierState method adds a state to the frontier.

Parameters:

s - the state to add

isExplored

public boolean isExplored(StateCache.State s)

The isExplored() method tests whether a given state has been explored before.

Parameters:

s - the cached state to test whether it is explored

Returns:

true if this state has been explored and had its outgoing edges computed; false otherwise

setExplored

public void setExplored(StateCache.State s)

The setExplored() method marks the given state as having been explored. A state cannot both be explored and be on the frontier; thus this method will throw a fatal error if the given state is marked as on the frontier.

Parameters:

s - the state to mark as explored

isFrontier

public boolean isFrontier(StateCache.State s)

The isFrontier() method tests whether a given state is currently in the frontier list of the state transition graph.

Parameters:

s - the state to test whether it is on the frontier

Returns:

true if the state is currently on the frontier of the state transition graph; false otherwise

getStateCache

public StateCache getStateCache()

The getStateCache() method gets the cache of all the states in the state space.

Returns:

a reference to the cache of all the states in the state transition graph

getEdenState

public StateCache.State getEdenState()

getFrontierCount

public long getFrontierCount()

getEdgeCount

public long getEdgeCount()

getExploredCount

public long getExploredCount()

newSet

public StateCache.Set newSet()

deleteStateSets

public void deleteStateSets()

dump

public void dump(Printer p)