public final class PaigeTarjanInitializers extends Object
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.
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.
|
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) |
public static void initCompleteDeterministic(PaigeTarjan pt, UniversalDeterministicAutomaton.FullIntAbstraction<?,?,?> absAutomaton, PaigeTarjanInitializers.AutomatonInitialPartitioning ip, boolean pruneUnreachable)
pt
- the partition refinement data structureabsAutomaton
- the abstraction of the input automatonip
- the initial partitioning modepruneUnreachable
- whether or not to prune unreachable states during initializationpublic static void initCompleteDeterministic(PaigeTarjan pt, SimpleDeterministicAutomaton.FullIntAbstraction absAutomaton, IntFunction<?> initialClassification, boolean pruneUnreachable)
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)
.
pt
- the partition refinement data structureabsAutomaton
- the abstraction of the input automatoninitialClassification
- the function determining the initial classificationpruneUnreachable
- whether or not to prune unreachable states during initializationpublic static void prefixSum(int[] array, int startInclusive, int endExclusive)
public static <S,I> StateIDs<S> initDeterministic(PaigeTarjan pt, SimpleDeterministicAutomaton<S,I> automaton, Alphabet<I> inputs, Function<? super S,?> initialClassification, Object sinkClassification)
This method can be used for automata with partially defined transition functions.
pt
- the partition refinement data structureautomaton
- the input automatoninputs
- the input alphabet to consider, which also determines the mapping from int
s to input symbols in
the data structureinitialClassification
- the initial classification functionsinkClassification
- determines how a sink is being classified.int
s representing states in the partition refinement data structure
to states of the automaton, and vice versapublic static <S,I,T> StateIDs<S> initDeterministic(PaigeTarjan pt, DeterministicAutomaton<S,I,T> automaton, Alphabet<I> inputs, Predicate<? super S> initialClassification, boolean sinkClassification)
This method can be used for automata with partially defined transition functions.
pt
- the partition refinement data structureautomaton
- the input automatoninputs
- the input alphabet to consider, which also determines the mapping from int
s to input symbols in
the data structureinitialClassification
- the initial classification predicatesinkClassification
- determines how a sink is being classified.int
s representing states in the partition refinement data structure
to states of the automaton, and vice versaCopyright © 2018. All rights reserved.