Package 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.

Method Summary

Modifier and Type	Method	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, AutomatonInitialPartitioning ip, boolean pruneUnreachable)	Initializes the partition refinement data structure from a given abstracted deterministic automaton, using a predefined initial partitioning mode.
static void	initDeterministic(PaigeTarjan pt, SimpleDeterministicAutomaton.FullIntAbstraction absAutomaton, IntFunction<?> 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,
                                             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 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 to prune unreachable states during initialization

prefixSum

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

initDeterministic

public static void initDeterministic(PaigeTarjan pt,
                                     SimpleDeterministicAutomaton.FullIntAbstraction absAutomaton,
                                     IntFunction<?> 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

absAutomaton - the abstraction of the input automaton

initialClassification - the initial classification function

sinkClassification - determines how a sink is being classified.