Package org.svvrl.goal.core.aut

Class DFS

java.lang.Object
org.svvrl.goal.core.aut.DFS
Direct Known Subclasses:
DoubleDFS, MSCCFinder.Finder
public class DFS
extends java.lang.Object
This class provides depth-first searches (DFS) in an automaton. The depth-first search is implemented by a stack. This class is not thread-safe. Do not invoke more than one DFS concurrently in the same DFS object. Note that if the automaton has disconnected states, those states may not be visited.
Author:
Ming-Hsien Tsai

  • Constructor Summary

    Constructors 
    Constructor Description
    DFS​(Automaton automaton)
    Constructs this DFS to search in an automaton.

  • Method Summary

    Modifier and Type Method Description
    void dfs()
    Performs a DFS in the input automaton from the initial states.
    void dfs​(java.util.Set<State> states)
    Performs a DFS in the input automaton from a specified set of states.
    void dfs​(State s)
    Performs a DFS in the input automaton from a specified state.
    Automaton getAutomaton()
    Returns the automaton where this DFS is performed.
    int getDFSNumber​(State s)
    Returns the DFS number of a state (starting from 0).
    StateSet getUnvisitedStates()
    Returns the unvisited states.
    StateSet getVisitedStates()
    Returns the visited states.
    boolean isVisitable​(State s)
    Returns true if a specified state can be visited.
    boolean isVisited​(State s)
    Returns true if a specified state was visited during some previous DFS.
    protected void onAllSuccessorsReturned​(StateList prefix, State curr)
    Invoked after the depth-first search of all successors of a state returns.
    protected void onSuccessorReturned​(StateList prefix, State curr, State succ)
    Invoked when returning from the depth-first search of a successor.
    protected void onVisitedStateFound​(StateList prefix, State curr, State visited)
    Invoked when a visited state is encountered.
    protected void onVisitState​(StateList prefix, State curr)
    Invoked when a state is visited at the first time.
    State proposeNextUnvisitedState()
    Proposes the next unvisited state for the start of a DFS.
    void reset()
    Resets this DFS.
    void setVisitable​(StateSet states)
    Makes this DFS visit only a specified set of states.

    Methods inherited from class java.lang.Object

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

  • Constructor Details

    • DFS

      public DFS​(Automaton automaton)
      Constructs this DFS to search in an automaton.
      Parameters:
      automaton - an automaton

  • Method Details

    • getAutomaton

      public Automaton getAutomaton()
      Returns the automaton where this DFS is performed.
      Returns:
      the automaton where this DFS is performed

    • setVisitable

      public void setVisitable​(StateSet states)
      Makes this DFS visit only a specified set of states.
      Parameters:
      states - a set of states that can be visited

    • isVisitable

      public boolean isVisitable​(State s)
      Returns true if a specified state can be visited.
      Parameters:
      s - a state
      Returns:
      true if the state can be visited

    • reset

      public void reset()
      Resets this DFS.

    • isVisited

      public boolean isVisited​(State s)
      Returns true if a specified state was visited during some previous DFS.
      Parameters:
      s - a state
      Returns:
      true if the state was visited during some previous DFS

    • getDFSNumber

      public int getDFSNumber​(State s)
      Returns the DFS number of a state (starting from 0).
      Parameters:
      s - a state
      Returns:
      the DFS number of a state, or -1 if the state was not visited in any performed DFS

    • getVisitedStates

      public StateSet getVisitedStates()
      Returns the visited states.
      Returns:
      a set of visited states

    • getUnvisitedStates

      public StateSet getUnvisitedStates()
      Returns the unvisited states. Note that states that cannot be visited will not be returned.
      Returns:
      a set of unvisited states
      See Also:
      setVisitable(StateSet)

    • onVisitState

      protected void onVisitState​(StateList prefix, State curr) throws FinishedException
      Invoked when a state is visited at the first time.
      Parameters:
      prefix - a path from the root to the current state curr
      curr - the current state to be visited
      Throws:
      FinishedException - if the depth-first search should stop here

    • onSuccessorReturned

      protected void onSuccessorReturned​(StateList prefix, State curr, State succ) throws FinishedException
      Invoked when returning from the depth-first search of a successor.
      Parameters:
      prefix - the path from the root to the current state curr
      curr - the current state
      succ - the successor of curr
      Throws:
      FinishedException - if the depth-first search should stop here

    • onAllSuccessorsReturned

      protected void onAllSuccessorsReturned​(StateList prefix, State curr) throws FinishedException
      Invoked after the depth-first search of all successors of a state returns.
      Parameters:
      prefix - the path from the root to the current state curr
      curr - the current state
      Throws:
      FinishedException - if the depth-first search should stop here

    • onVisitedStateFound

      protected void onVisitedStateFound​(StateList prefix, State curr, State visited) throws FinishedException
      Invoked when a visited state is encountered.
      Parameters:
      prefix - a path from the root to the current state curr
      curr - the current state which is the last state in prefix
      visited - the state that has been visited. It must be a successor of curr.
      Throws:
      FinishedException - if the depth-first search should stop here

    • proposeNextUnvisitedState

      public State proposeNextUnvisitedState()
      Proposes the next unvisited state for the start of a DFS. Below is the priority of the proposed states.
      1. Initial state.
      2. State that has no predecessor or have itself as the only predecessor.
      3. Other state
      Returns:
      an unvisited state, or null if all states were visited

    • dfs

      public void dfs()
      Performs a DFS in the input automaton from the initial states.

    • dfs

      public void dfs​(State s)
      Performs a DFS in the input automaton from a specified state.
      Parameters:
      s - the start of the DFS

    • dfs

      public void dfs​(java.util.Set<State> states)
      Performs a DFS in the input automaton from a specified set of states.
      Parameters:
      states - the starts of the DFS