net.automatalib.util.partitionrefinement

Class PaigeTarjanInitializers

java.lang.Object

net.automatalib.util.partitionrefinement.PaigeTarjanInitializers

public final class PaigeTarjanInitializers
extends Object

This class provides several methods to initialize a PaigeTarjan partition refinement data structure from common sources, e.g., automata.

The counterpart of this class is PaigeTarjanExtractors, which provides methods to translate the contents of the partition refinement data structure after coarsest stable partition computation back to such structures.

Author:

Malte Isberner

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	PaigeTarjanInitializers.AutomatonInitialPartitioning This enum allows to conveniently specify how the states of a deterministic automaton are initially partitioned when initializing the partition refinement data structure.

Method Summary

Modifier and Type	Method and Description
static void	initCompleteDeterministic(PaigeTarjan pt, SimpleDeterministicAutomaton.FullIntAbstraction absAutomaton, IntFunction<?> initialClassification, boolean pruneUnreachable) Initializes the partition refinement data structure from a given abstracted deterministic automaton, partitioning states according to the given classification function.
static void	initCompleteDeterministic(PaigeTarjan pt, UniversalDeterministicAutomaton.FullIntAbstraction<?,?,?> absAutomaton, PaigeTarjanInitializers.AutomatonInitialPartitioning ip, boolean pruneUnreachable) Initializes the partition refinement data structure from a given abstracted deterministic automaton, using a predefined initial partitioning mode.
static <S,I,T> StateIDs<S>	initDeterministic(PaigeTarjan pt, DeterministicAutomaton<S,I,T> automaton, Alphabet<I> inputs, Predicate<? super S> initialClassification, boolean sinkClassification) Initializes the partition refinement data structure from a given deterministic automaton, initializing the initial partition according to the given classification predicate (i.e., assuming a binary initial partitioning).
static <S,I> StateIDs<S>	initDeterministic(PaigeTarjan pt, SimpleDeterministicAutomaton<S,I> automaton, Alphabet<I> inputs, Function<? super S,?> initialClassification, Object sinkClassification) Initializes the partition refinement data structure from a given deterministic automaton, initializing the initial partition according to the given classification function.
static void	prefixSum(int[] array, int startInclusive, int endExclusive)

Methods inherited from class java.lang.Object

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

Method Detail

initCompleteDeterministic

public static void initCompleteDeterministic(PaigeTarjan pt,
                                             UniversalDeterministicAutomaton.FullIntAbstraction<?,?,?> absAutomaton,
                                             PaigeTarjanInitializers.AutomatonInitialPartitioning ip,
                                             boolean pruneUnreachable)

Initializes the partition refinement data structure from a given abstracted deterministic automaton, using a predefined initial partitioning mode.

Parameters:

pt - the partition refinement data structure

absAutomaton - the abstraction of the input automaton

ip - the initial partitioning mode

pruneUnreachable - whether or not to prune unreachable states during initialization

initCompleteDeterministic

public static void initCompleteDeterministic(PaigeTarjan pt,
                                             SimpleDeterministicAutomaton.FullIntAbstraction absAutomaton,
                                             IntFunction<?> initialClassification,
                                             boolean pruneUnreachable)

Initializes the partition refinement data structure from a given abstracted deterministic automaton, partitioning states according to the given classification function.

The return value of the initialClassification function can be any valid Object reference (even null). States are initially placed in the same partition class if their return values from applying initialClassification have the same hash code (determined according to Objects.hashCode(Object)) and are equal (determined according to Objects.equals(Object, Object).

Parameters:

pt - the partition refinement data structure

absAutomaton - the abstraction of the input automaton

initialClassification - the function determining the initial classification

pruneUnreachable - whether or not to prune unreachable states during initialization

prefixSum

public static void prefixSum(int[] array,
                             int startInclusive,
                             int endExclusive)

initDeterministic

public static <S,I> StateIDs<S> initDeterministic(PaigeTarjan pt,
                                                  SimpleDeterministicAutomaton<S,I> automaton,
                                                  Alphabet<I> inputs,
                                                  Function<? super S,?> initialClassification,
                                                  Object sinkClassification)

Initializes the partition refinement data structure from a given deterministic automaton, initializing the initial partition according to the given classification function.

This method can be used for automata with partially defined transition functions.

Parameters:

pt - the partition refinement data structure

automaton - the input automaton

inputs - the input alphabet to consider, which also determines the mapping from ints to input symbols in the data structure

initialClassification - the initial classification function

sinkClassification - determines how a sink is being classified.

Returns:

the state ID mapping relating ints representing states in the partition refinement data structure to states of the automaton, and vice versa

initDeterministic

public static <S,I,T> StateIDs<S> initDeterministic(PaigeTarjan pt,
                                                    DeterministicAutomaton<S,I,T> automaton,
                                                    Alphabet<I> inputs,
                                                    Predicate<? super S> initialClassification,
                                                    boolean sinkClassification)

Initializes the partition refinement data structure from a given deterministic automaton, initializing the initial partition according to the given classification predicate (i.e., assuming a binary initial partitioning).

This method can be used for automata with partially defined transition functions.

Parameters:

pt - the partition refinement data structure

automaton - the input automaton

inputs - the input alphabet to consider, which also determines the mapping from ints to input symbols in the data structure

initialClassification - the initial classification predicate

sinkClassification - determines how a sink is being classified.

Returns:

the state ID mapping relating ints representing states in the partition refinement data structure to states of the automaton, and vice versa