public 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.
|
Constructor and Description |
---|
PaigeTarjanInitializers() |
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.
|
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 <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 © 2015. All rights reserved.