Package owl.automaton.algorithm.simulations

Class ColorRefinement.Neighborhood

java.lang.Object

owl.automaton.algorithm.simulations.ColorRefinement.Neighborhood

Enclosing class:

ColorRefinement<S>

public abstract static class ColorRefinement.Neighborhood
extends Object

Represents the neighborhood of a state. A neighborhood consists of all NeighborTypes that are maximal with regard to the ordering computed in the previous iteration.

Constructor Summary

Constructors

Constructor	Description
Neighborhood()

Method Summary

Modifier and Type	Method	Description
abstract BddSet	available()
int	compareTo(ColorRefinement.Neighborhood other)	Compares a neighborhood to another such that they can be sorted.
boolean	dominates(owl.automaton.algorithm.simulations.ColorRefinement.Ordering ord, ColorRefinement.Neighborhood other)	Tests whether the neighborhood dominates another, which holds if each neighbor type in the other neighborhood is dominated by one in this neighborhood.
static <S> ColorRefinement.Neighborhood	maximal(Automaton<S,BuchiAcceptance> aut, S state, owl.automaton.algorithm.simulations.ColorRefinement.Ordering ord, owl.automaton.algorithm.simulations.ColorRefinement.Coloring<S> col)	Constructs a neighborhood for a given state under a previously computed coloring and ordering consisting of only maximal NeighborTypes.
static ColorRefinement.Neighborhood	of(Set<ColorRefinement.NeighborType> nts, BddSet available)
abstract Set<ColorRefinement.NeighborType>	types()

Methods inherited from class java.lang.Object

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

Constructor Detail

Neighborhood

public Neighborhood()

Method Detail

types

public abstract Set<ColorRefinement.NeighborType> types()

available

public abstract BddSet available()

of

public static ColorRefinement.Neighborhood of(Set<ColorRefinement.NeighborType> nts,
                                              BddSet available)

compareTo

public int compareTo(ColorRefinement.Neighborhood other)

Compares a neighborhood to another such that they can be sorted.

Parameters:

other - The neighborhood to compare against.

Returns:

0 if they are equal, -1 if the other is larger, 1 otherwise.

maximal

public static <S> ColorRefinement.Neighborhood maximal(Automaton<S,BuchiAcceptance> aut,
                                                       S state,
                                                       owl.automaton.algorithm.simulations.ColorRefinement.Ordering ord,
                                                       owl.automaton.algorithm.simulations.ColorRefinement.Coloring<S> col)

Constructs a neighborhood for a given state under a previously computed coloring and ordering consisting of only maximal NeighborTypes.

Type Parameters:

S - Type of state of the automaton.

Parameters:

aut - The underlying automaton.

state - The state to compute the maximal Neighborhood for.

ord - Ordering with regard to which maximality is tested.

col - The coloring associated with the Ordering.

Returns:

A maximal neighborhood where no type is dominated by another.

dominates

public boolean dominates(owl.automaton.algorithm.simulations.ColorRefinement.Ordering ord,
                         ColorRefinement.Neighborhood other)

Tests whether the neighborhood dominates another, which holds if each neighbor type in the other neighborhood is dominated by one in this neighborhood.

Parameters:

ord - The order to compare against.

other - The other neighborhood that is dominated.

Returns:

True if and only if this neighborhood dominates the other.