net.automatalib.util.partitionrefinement

Class PaigeTarjanExtractors

java.lang.Object

net.automatalib.util.partitionrefinement.PaigeTarjanExtractors

public final class PaigeTarjanExtractors
extends Object

This class provides methods for translating the result of a PaigeTarjan coarsest stable partition computation into several common, more usable forms such as automata.

Most of the methods defined in this class expect the partition data to be in a certain form, and moreover may require additional information, both of which is provided by corresponding methods defined in PaigeTarjanInitializers.

Author:

Malte Isberner

Method Summary

Modifier and Type	Method and Description
static <I,T,SP,TP,A extends MutableDeterministic<?,I,?,SP,TP>> A	toDeterministic(PaigeTarjan pt, AutomatonCreator<A,I> creator, Alphabet<I> inputs, DeterministicAutomaton.FullIntAbstraction<T> absOriginal, IntFunction<? extends SP> spExtractor, Function<? super T,? extends TP> tpExtractor, boolean pruneUnreachable) Translates the results of a coarsest stable partition computation into a deterministic automaton.
static <S1,S2,I,T1,T2,SP,TP,A extends MutableDeterministic<S2,I,T2,SP,TP>> A	toDeterministic(PaigeTarjan pt, AutomatonCreator<A,I> creator, Alphabet<I> inputs, DeterministicAutomaton<S1,I,T1> original, StateIDs<S1> origIds, Function<? super S1,? extends SP> spExtractor, Function<? super T1,? extends TP> tpExtractor, boolean pruneUnreachable) Translates the results of a coarsest stable partition computation into a deterministic automaton.

Methods inherited from class java.lang.Object

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

Method Detail

toDeterministic

public static <S1,S2,I,T1,T2,SP,TP,A extends MutableDeterministic<S2,I,T2,SP,TP>> A toDeterministic(PaigeTarjan pt,
                                                                                                    AutomatonCreator<A,I> creator,
                                                                                                    Alphabet<I> inputs,
                                                                                                    DeterministicAutomaton<S1,I,T1> original,
                                                                                                    StateIDs<S1> origIds,
                                                                                                    Function<? super S1,? extends SP> spExtractor,
                                                                                                    Function<? super T1,? extends TP> tpExtractor,
                                                                                                    boolean pruneUnreachable)

Translates the results of a coarsest stable partition computation into a deterministic automaton.

This method is designed to match the following methods from PaigeTarjanInitializers:

• PaigeTarjanInitializers.initDeterministic(PaigeTarjan, net.automatalib.automata.simple.SimpleDeterministicAutomaton,Alphabet, Function, Object)
• PaigeTarjanInitializers.initDeterministic(PaigeTarjan,DeterministicAutomaton, Alphabet, java.util.function.Predicate, boolean)

Both the spExtractor and the tpExtractor can be null, in which case they are replaced by a function always returning null.

Parameters:

pt - the partition refinement data structure, after computing the coarsest stable partition

creator - an AutomatonCreator for creating the resulting automaton

inputs - the input alphabet to use

original - the original automaton on which the partition was computed

origIds - the StateIDs that translate the ints from the PaigeTarjan to states of original (e.g., obtained as the result from PaigeTarjanInitializers.initDeterministic(PaigeTarjan, DeterministicAutomaton, Alphabet, java.util.function.Predicate, boolean)

spExtractor - the state property extractor, or null

tpExtractor - the transition property extractor, or null

pruneUnreachable - true if unreachable states should be pruned during construction, false otherwise

Returns:

an automaton created using the specified creator, over the specified input alphabet, and reflecting the partition data of the specified PaigeTarjan object

toDeterministic

public static <I,T,SP,TP,A extends MutableDeterministic<?,I,?,SP,TP>> A toDeterministic(PaigeTarjan pt,
                                                                                        AutomatonCreator<A,I> creator,
                                                                                        Alphabet<I> inputs,
                                                                                        DeterministicAutomaton.FullIntAbstraction<T> absOriginal,
                                                                                        IntFunction<? extends SP> spExtractor,
                                                                                        Function<? super T,? extends TP> tpExtractor,
                                                                                        boolean pruneUnreachable)

Translates the results of a coarsest stable partition computation into a deterministic automaton.

This method is designed to match the following methods from PaigeTarjanInitializers:

• PaigeTarjanInitializers.initCompleteDeterministic(PaigeTarjan, net.automatalib.automata.simple.SimpleDeterministicAutomaton.FullIntAbstraction, IntFunction, boolean)
• PaigeTarjanInitializers.initCompleteDeterministic(PaigeTarjan, net.automatalib.automata.UniversalDeterministicAutomaton.FullIntAbstraction, PaigeTarjanInitializers.AutomatonInitialPartitioning, boolean)

Both the spExtractor and the tpExtractor can be null, in which case they are replaced by a function always returning null.

Parameters:

pt - the partition refinement data structure, after computing the coarsest stable partition

creator - an AutomatonCreator for creating the resulting automaton

inputs - the input alphabet to use

absOriginal - the abstraction of the original automaton that was used to build the partition refinement data structure

spExtractor - the state property extractor, or null

tpExtractor - the transition property extractor, or null

pruneUnreachable - true if unreachable states should be pruned during construction, false otherwise

Returns:

an automaton created using the specified creator, over the specified input alphabet, and reflecting the partition data of the specified PaigeTarjan object