Package org.svvrl.goal.core.aut

Class DoubleDFSTraverser

java.lang.Object
org.svvrl.goal.core.aut.DFSTraverser
org.svvrl.goal.core.aut.DoubleDFSTraverser
public abstract class DoubleDFSTraverser
extends DFSTraverser
Deprecated.
use DoubleDFS instead
A DoubleDFSTraverser can traverse an automaton by a double depth-first search. The implementation is based on recursive calls.
Author:
Ming-Hsien Tsai

  • Constructor Details

    • DoubleDFSTraverser

      public DoubleDFSTraverser​(Automaton aut)
      Deprecated.
      Constructor.
      Parameters:
      aut - the automaton to be traversed

  • Method Details

    • goDFS2

      protected abstract boolean goDFS2​(StateList prefix, State s)
      Deprecated.
      Checks if a second DFS should start from this state or not.
      Parameters:
      prefix - the traversed prefix in the first DFS
      s - the current state
      Returns:
      true if the second DFS should start here

    • visitDFS2State

      protected abstract void visitDFS2State​(State s)
      Deprecated.
      Invoked when a state is visited in the second DFS.
      Parameters:
      s - a state visited in the second DFS

    • isLassoAccepted

      protected abstract boolean isLassoAccepted​(StateRun run)
      Deprecated.
      Check if a lasso found in the second DFS is accepted or not.
      Parameters:
      run - the lasso
      Returns:
      true if the lasso is accepted by this double DFS

    • onAllSuccessorsReturned

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