Package org.svvrl.goal.core.aut

Class DoubleDFS

java.lang.Object

org.svvrl.goal.core.aut.DFS

org.svvrl.goal.core.aut.DoubleDFS

Direct Known Subclasses:

AcceptingRunFinder, InputTester.AcceptingRunFinder

public abstract class DoubleDFS
extends DFS

This class provides double depth-first searches in an automaton for finding accepting lassos. The depth-first search is implemented by a stack.

Author:

Ming-Hsien Tsai

Constructor Summary

Constructors

Constructor	Description
DoubleDFS(Automaton automaton)	Constructs this double DFS to search in an automaton.

Method Summary

Modifier and Type	Method	Description
protected abstract boolean	goDFS2(StateList prefix, State curr)	Returns true if a second DFS should start from a specified state.
protected abstract boolean	isLassoAccepted(StateRun run)	Returns true if a lasso found in the second DFS is accepted.
protected void	onAllSuccessorsReturned(StateList prefix, State curr)	Invoked after the depth-first search of all successors of a state returns.
protected void	onVisitDFS2State(StateList path1, StateList path2, State curr)	Invoked when a state is visited in the second DFS.

Methods inherited from class org.svvrl.goal.core.aut.DFS

dfs, dfs, dfs, getAutomaton, getDFSNumber, getUnvisitedStates, getVisitedStates, isVisitable, isVisited, onSuccessorReturned, onVisitedStateFound, onVisitState, proposeNextUnvisitedState, reset, setVisitable

Methods inherited from class java.lang.Object

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

Constructor Details

DoubleDFS

public DoubleDFS(Automaton automaton)

Constructs this double DFS to search in an automaton.

Parameters:

automaton - an automaton

Method Details

goDFS2

protected abstract boolean goDFS2(StateList prefix, State curr)

Returns true if a second DFS should start from a specified state.

Parameters:

prefix - the traversed prefix in the first DFS

curr - the current state

Returns:

true if the second DFS should start from the current state

onVisitDFS2State

protected void onVisitDFS2State(StateList path1, StateList path2, State curr)

Invoked when a state is visited in the second DFS.

Parameters:

path1 - the path from the root to the start state of the second DFS

path2 - the path from the start state of the second DFS to the current state

curr - a state currently visited in the second DFS

isLassoAccepted

protected abstract boolean isLassoAccepted(StateRun run)

Returns true if a lasso found in the second DFS is accepted.

Parameters:

run - a lasso

Returns:

true if the lasso is accepted by this double DFS

onAllSuccessorsReturned

protected void onAllSuccessorsReturned(StateList prefix, State curr) throws FinishedException

Description copied from class: DFS

Invoked after the depth-first search of all successors of a state returns.

Overrides:

onAllSuccessorsReturned in class DFS

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