Overview | Package | Class | Tree | Deprecated | Index | Help
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## avrora.stack
Class StateSpace

    java.lang.Object
      avrora.stack.StateSpace

public class StateSpace
extends java.lang.Object

The `StateSpace` class represents the reachable state space as it is explored by the `Analyzer` class. It stores reachable states and the outgoing edges that connect them.

Nested Class Summary
`class` | `StateSpace.Link` The `Link` inner class represents an edge between two states within the state space.
`class` | `StateSpace.State` The `State` class represents an immutable state within the state space of the program.

Constructor Summary
`StateSpace(Program p)` The constructor for the `StateSpace` accepts a program as a parameter.

Method Summary
`void` | `addEdge(StateSpace.State s, StateSpace.State t)` The `addEdge()` method creates an edge between the specified states with weight 0.
`void` | `addEdge(StateSpace.State s, StateSpace.State t, int weight)` The `addEdge()` method creates an edge between the specified states with the given weight.
`boolean` | `addFrontier(StateSpace.State s)` The `addFrontier` method adds a state to the frontier.
`boolean` | `addState(StateSpace.State s)` The `addState()` method adds a state to the state space (marks it as explored).
`StateSpace.State` | `getEdenState()` The `getEdenState()` method gets the starting state of the abstract interpretation.
`StateSpace.State` | `getFrontierState()` The `getFrontierState()` chooses a state off of the state frontier, removes it from the state frontier, and returns it.
`long` | `getSpecialStateCount()` The `getSpecialStateCount()` method returns the number of special states that were created.
`StateSpace.State` | `getStateFor(MutableState s)` The `getStateFor()` method searches the state cache for an immutable state that corresponds to the given mutable state.
`long` | `getStatesInSpaceCount()` The `getStatesInSpaceCount()` method returns the number of unique states that have been added to this state space.
`long` | `getTotalStateCount()` The `getTotalStateCount()` method returns the internally recorded number of states created in this state space.
`boolean` | `isExplored(StateSpace.State s)` The `isExplored()` method checks whether the specified state has been added to this state space (i.e. it has been explored).
`boolean` | `isFrontier(StateSpace.State s)` The `isFrontier()` method checks whether the specified state is currently on the state frontier.
`avrora.stack.StateSpace.SpecialState` | `makeSpecialState(java.lang.String name)` The `makeSpecialState()` method creates a special state that represents something important to an analysis tool, such as a RETURN state.

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Constructor Detail

### StateSpace

    public StateSpace(Program p)

  The constructor for the `StateSpace` accepts a program as a parameter. This is currently unused, but is reserved for use later.

Parameters:
  `p` - the program to create the state space for

Method Detail

### getEdenState

    public StateSpace.State getEdenState()

  The `getEdenState()` method gets the starting state of the abstract interpretation.

  Returns:
    the initial state to begin abstract interpretation

### getFrontierState

    public StateSpace.State getFrontierState()

  The `getFrontierState()` 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 there are no states on the frontier, not even the eden state.

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

### isExplored

    public boolean isExplored(StateSpace.State s)

  The `isExplored()` method checks whether the specified state has been added to this state space (i.e. it has been explored). A state can be added at most once and cannot be removed from the state space.

  Parameters:
    `s` - the state to check
  Returns:
    true if the specified state has been explored; false otherwise

### isFrontier

    public boolean isFrontier(StateSpace.State s)

  The `isFrontier()` method checks whether the specified state is currently on the state frontier.

  Parameters:
    `s` - the state to check
  Returns:
    true if the specified state is currently on the frontier; false otherwise

### addState

    public boolean addState(StateSpace.State s)

  The `addState()` method adds a state to the state space (marks it as explored). A state can be added at most once and cannot be removed once it has been added. Note that being cached does not imply that the state is in the state space.

  Parameters:
    `s` - the state to add to the state space.
  Returns:
    true if this state is already in the state space; false otherwise

### addFrontier

    public boolean addFrontier(StateSpace.State s)

  The `addFrontier` method adds a state to the frontier.

  Parameters:
    `s` - the state to add
  Returns:
    true if the state was already on the frontier; false otherwise

### makeSpecialState

    public avrora.stack.StateSpace.SpecialState makeSpecialState(java.lang.String name)

  The `makeSpecialState()` method creates a special state that represents something important to an analysis tool, such as a RETURN state. These special states are not stored in the state cache.

  Parameters:
    `name` - the name of the special state
  Returns:
    an instance of the `SpecialState` class that is the newly created special states.

### getStateFor

    public StateSpace.State getStateFor(MutableState s)

  The `getStateFor()` method searches the state cache for an immutable state that corresponds to the given mutable state. If no immutable state exists in the cache, one will be created and inserted.

  Parameters:
    `s` - the state to search for
  Returns:
    an instance of the `StateSpace.State` immutable state that corresponds to the given mutable state

### addEdge

    public void addEdge(StateSpace.State s,
                        StateSpace.State t,
                        int weight)

  The `addEdge()` method creates an edge between the specified states with the given weight. No checking for duplicate edges is done.

  Parameters:
    `s` - the source state
    `t` - the destination state
    `weight` - the weight to assign to the edge

### addEdge

    public void addEdge(StateSpace.State s,
                        StateSpace.State t)

  The `addEdge()` method creates an edge between the specified states with weight 0. No checking for duplicate edges is done.

  Parameters:
    `s` - the source state
    `t` - the destination state

### getTotalStateCount

    public long getTotalStateCount()

  The `getTotalStateCount()` method returns the internally recorded number of states created in this state space. This is mainly used for reporting purposes.

  Returns:
    the total number of states in the state cache

### getStatesInSpaceCount

    public long getStatesInSpaceCount()

  The `getStatesInSpaceCount()` method returns the number of unique states that have been added to this state space. This is mainly used for reporting purposes.

  Returns:
    the number of states added to the state space

### getSpecialStateCount

    public long getSpecialStateCount()

  The `getSpecialStateCount()` method returns the number of special states that were created. This is mainly used for reporting purposes.

  Returns:
    the number of special states created

Overview | Package | Class | Tree | Deprecated | Index | Help
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD