Package org.svvrl.goal.core.comp.wdbw

Class DeterminizationToWDBWByDEK07

java.lang.Object

org.svvrl.goal.core.AbstractAlgorithm

org.svvrl.goal.core.AbstractControllableAlgorithm

org.svvrl.goal.core.AbstractEditableAlgorithm

org.svvrl.goal.core.comp.wdbw.DeterminizationToWDBWByDEK07

All Implemented Interfaces:

java.util.EventListener, Algorithm, AlgorithmListener, ControllableAlgorithm, EditableAlgorithm

public class DeterminizationToWDBWByDEK07
extends AbstractEditableAlgorithm

This class implements the algorithm of determinizing an ω-automaton to an equivalent WDBW if any equivalent WDBW exists [Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Powerset Construction for Restricted Classes of omega -Automata. ATVA 2007: 223-236].

Author:

Ming-Hsien Tsai

Constructor Summary

Constructors

Constructor	Description
DeterminizationToWDBWByDEK07(FSA aut)	Constructs this object to convert an input ω-automaton to an equivalent WDBW.

Method Summary

Modifier and Type	Method	Description
Editable	getIntermediateResult()	Returns the intermediate result.
FSA	getResult()	Returns an equivalent WDBW of the input automaton.

Methods inherited from class org.svvrl.goal.core.AbstractControllableAlgorithm

addControllableListener, addSubAlgorithm, doPause, doStage, doStart, doStep, fireReferenceChangedEvent, getInterval, getStages, getStatus, pause, pause, removeControllableListener, removeSubAlgorithm, setInterval, setStages, setStatus, setSynchronizationObject, stagePause, stagePause

Methods inherited from class org.svvrl.goal.core.AbstractAlgorithm

addAlgorithmListener, addProgress, appendStageMessage, appendStepMessage, getAlgorithmListeners, getCurrentProgress, getMaximalProgress, getMinimalProgress, getName, getOptions, getSubAlgorithms, isDeterministicProgress, removeAlgorithmListener, setCurrentProgress, setDeterministicProgress, setMaximalProgress, setMinimalProgress

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.svvrl.goal.core.Algorithm

addAlgorithmListener, getAlgorithmListeners, getOptions, removeAlgorithmListener

Methods inherited from interface org.svvrl.goal.core.AlgorithmListener

appendStageMessage, appendStepMessage, getCurrentProgress, getMaximalProgress, getMinimalProgress, setCurrentProgress, setDeterministicProgress, setMaximalProgress, setMinimalProgress

Methods inherited from interface org.svvrl.goal.core.ControllableAlgorithm

addControllableListener, doPause, doStage, doStart, doStep, getInterval, getStages, getStatus, removeControllableListener, setInterval, setStages, setStatus, setSynchronizationObject

Constructor Details

DeterminizationToWDBWByDEK07

public DeterminizationToWDBWByDEK07(FSA aut) throws java.lang.IllegalArgumentException

Constructs this object to convert an input ω-automaton to an equivalent WDBW.

Parameters:

aut - an ω-automaton

Throws:

java.lang.IllegalArgumentException - if the input automaton is not an ω-automaton

Method Details

getResult

public FSA getResult() throws java.lang.IllegalArgumentException

Returns an equivalent WDBW of the input automaton.

Returns:

an equivalent WDBW of the input automaton

Throws:

java.lang.IllegalArgumentException - if the input automaton is not equivalent to any WDBW

getIntermediateResult

public Editable getIntermediateResult()

Description copied from interface: EditableAlgorithm

Returns the intermediate result.

Returns:

the intermediate result of this algorithm