de.uni_due.inf.ti.raven.algorithms

Class SimulationAntichainUniversality

java.lang.Object

de.uni_due.inf.ti.raven.algorithms.SimulationAntichainUniversality

All Implemented Interfaces:

Algorithm, UniversalityAlgorithm

public final class SimulationAntichainUniversality
extends Object
implements UniversalityAlgorithm

This class implements the two simulation-based antichain algorithms deciding the universality problem for (finite) automata. The algorithms are based on the work of Abdulla et. al. More details about the algorithms can be found in "When Simulation Meets Antichains (on Checking Language Inclusion on NFAs)" Homepage of Parosh Aziz Abdulla.

Version:

$Revision: 1.44 $

Author:

Christoph Blume, Laura Steinert

Nested Class Summary

Nested classes/interfaces inherited from interface de.uni_due.inf.ti.raven.algorithms.UniversalityAlgorithm

UniversalityAlgorithm.Implementations

Nested classes/interfaces inherited from interface de.uni_due.inf.ti.raven.algorithms.Algorithm

Algorithm.OrderingType, Algorithm.SearchType

Field Summary

Fields inherited from interface de.uni_due.inf.ti.raven.algorithms.UniversalityAlgorithm

UNIVERSALITY_ITERATION_STEP

Constructor Summary

Constructors

Constructor and Description
SimulationAntichainUniversality(Algorithm.SearchType searchType) Creates a new instance of the antichain-based universality algorithm.
SimulationAntichainUniversality(Algorithm.SearchType searchType, Algorithm.OrderingType orderingType) Creates a new instance of the antichain-based universality algorithm.
SimulationAntichainUniversality(Algorithm.SearchType searchType, Algorithm.OrderingType orderingType, boolean computeCounterExample) Creates a new instance of the antichain-based universality algorithm.

Method Summary

Methods

Modifier and Type	Method and Description
void	addComputationListener(ComputationListener l) Adds the Computation Listener l to this algorithm.
void	cancelComputation() Cancels the computation of this algorithm.
CospanCounterExample	getCounterExample() Returns the counter example, if the language of the automaton is not universal and null otherwise
boolean	isUniversal(Automaton automaton) Returns true if and only if the automaton automaton is universal.
void	removeComputationListener(ComputationListener l) Removes the Computation Listener l from this algorithm.

Methods inherited from class java.lang.Object

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

Constructor Detail

SimulationAntichainUniversality

public SimulationAntichainUniversality(Algorithm.SearchType searchType,
                               Algorithm.OrderingType orderingType,
                               boolean computeCounterExample)

Creates a new instance of the antichain-based universality algorithm.

Parameters:

searchType - the search type used by the algorithm, either forward or backward

orderingType - the ordering type used by the algorithm either identityRelation, forwardSimulation or backwardSimulation

computeCounterExample - if true a counterexample will be computed if the input language is not universal

See Also:

Algorithm.SearchType, Algorithm.OrderingType

SimulationAntichainUniversality

public SimulationAntichainUniversality(Algorithm.SearchType searchType,
                               Algorithm.OrderingType orderingType)

Creates a new instance of the antichain-based universality algorithm.

Parameters:

searchType - the search type used by the algorithm, either forward or backward

orderingType - the ordering type used by the algorithm either identityRelation, forwardSimulation or backwardSimulation

See Also:

Algorithm.SearchType, Algorithm.OrderingType

SimulationAntichainUniversality

public SimulationAntichainUniversality(Algorithm.SearchType searchType)

Creates a new instance of the antichain-based universality algorithm.

Parameters:

searchType - the search type used by the algorithm, either forward or backward

See Also:

Algorithm.SearchType

Method Detail

addComputationListener

public void addComputationListener(ComputationListener l)

Description copied from interface: Algorithm

Adds the Computation Listener l to this algorithm.

Specified by:

addComputationListener in interface Algorithm

Parameters:

l - the listener to receive computation events

removeComputationListener

public void removeComputationListener(ComputationListener l)

Description copied from interface: Algorithm

Removes the Computation Listener l from this algorithm.

Specified by:

removeComputationListener in interface Algorithm

Parameters:

l - the listener to be removed

isUniversal

public boolean isUniversal(Automaton automaton)

Description copied from interface: UniversalityAlgorithm

Returns true if and only if the automaton automaton is universal.

Specified by:

isUniversal in interface UniversalityAlgorithm

Parameters:

automaton - the automaton to be checked

Returns:

true if the automaton is universal, false otherwise

getCounterExample

public CospanCounterExample getCounterExample()

Description copied from interface: UniversalityAlgorithm

Returns the counter example, if the language of the automaton is not universal and null otherwise

Specified by:

getCounterExample in interface UniversalityAlgorithm

Returns:

the counter example (if the universality check failed) or null otherwise

cancelComputation

public void cancelComputation()

Description copied from interface: Algorithm

Cancels the computation of this algorithm.

Specified by:

cancelComputation in interface Algorithm