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 | 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,
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) |
public static void initCompleteDeterministic(PaigeTarjan pt, UniversalDeterministicAutomaton.FullIntAbstraction<?,?,?> absAutomaton, 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 void initDeterministic(PaigeTarjan pt, SimpleDeterministicAutomaton.FullIntAbstraction absAutomaton, IntFunction<?> initialClassification, Object sinkClassification)
This method can be used for automata with partially defined transition functions.
pt
- the partition refinement data structureabsAutomaton
- the abstraction of the input automatoninitialClassification
- the initial classification functionsinkClassification
- determines how a sink is being classified.Copyright © 2020. All rights reserved.