All Classes

Class	Description
AbstractAlphabet<I>
AbstractCompact<I,T,SP,TP>	Abstract super class for compact automata representations.
AbstractCompact.Payload	A utility class that encapsulates necessary information for performing an update of the stored automata data.
AbstractCompactBidiGraph<NP,EP>
AbstractCompactDeterministic<I,T,SP,TP>	Abstract super class that refines AbstractCompact for deterministic automata.
AbstractCompactGraph<E extends CompactEdge<EP>,NP,EP>
AbstractCompactMTS<I,T,TP extends MutableModalEdgeProperty>	An abstract base-implementation for MutableModalTransitionSystems.
AbstractCompactSimpleDeterministic<I,SP>	Abstract super class that refines AbstractCompactDeterministic for transition-property-less automata.
AbstractCompactSimpleNondet<I,SP>	Abstract super class that refines AbstractCompact for transition-property-less automata.
AbstractDefaultSEVPA<I>	Basic functionality for Location-based SEVPA implementations.
AbstractFastMutable<S extends AbstractFastState<?>,I,T,SP,TP>	Shared functionality for (non-) deterministic mutable automata.
AbstractFastMutableDet<S extends AbstractFastState<T>,I,T,SP,TP>
AbstractFastMutableNondet<S extends AbstractFastState<Collection<T>>,I,T,SP,TP>
AbstractFastState<T>
AbstractLasso<I,D>
AbstractRecursiveADSLeafNode<S,I,O,N extends RecursiveADSNode<S,I,O,N>>	An abstract implementation of a leaf node, that may be used by other ADS-extending classes.
AbstractRecursiveADSSymbolNode<S,I,O,N extends RecursiveADSNode<S,I,O,N>>	An abstract implementation of a symbol node, that may be used by other ADS-extending classes.
AbstractSEVPA<L,I>	Abstract class for k-SEVPAs that implements functionality shared across different subtypes.
AbstractSymbol<S extends AbstractSymbol<S>>
AbstractUnfoldingModelChecker<I,A,P,L extends Lasso<I,?>>	An ModelCheckerLasso that can unfold loops of lassos.
AbstractVPAlphabet<I>	Abstract utility class that implements functionality shared across different subtypes.
ADSLeafNode<S,I,O>	An ADS-specific implementation of a leaf node.
ADSSymbolNode<S,I,O>	An ADS-specific implementation of a symbol node.
AggregateVisualizationHelper<N,E>
Alphabets	Utility methods concerning alphabets.
ArrayAlphabet<I>
CompactBidiEdge<EP>
CompactBidiGraph<NP,EP>
CompactDFA<I>
CompactDFA.Creator<I>
CompactEdge<EP>	An edge in a CompactSimpleGraph.
CompactGraph<NP,EP>
CompactMealy<I,O>
CompactMealy.Creator<I,O>
CompactMoore<I,O>
CompactMoore.Creator<I,O>
CompactMTS<I>
CompactNFA<I>
CompactNFA.Creator<I>
CompactPMPG<L,AP>
CompactPMPGEdge<L,EP>
CompactSimpleBidiGraph<EP>
CompactSimpleGraph<EP>
CompactSST<I,O>
CompactTransition<TP>
DefaultCFMPS<L,AP>
DefaultNSEVPA<I>	Default implementation for n-SEVPAs.
DefaultOneSEVPA<I>	Default implementation for 1-SEVPAs.
DefaultProceduralInputAlphabet<I>	Default implementation of a ProceduralInputAlphabet.
DefaultProceduralOutputAlphabet<O>	Default implementation of a ProceduralOutputAlphabet.
DefaultVPAlphabet<I>	An alphabet-based, fixed size implementation of a VPAlphabet.
DeterministicPowersetView<S,I,T>
DFALassoImpl<I>	A DFALasso is a lasso for DFAs.
DummyVP
EmptySBA<I>	A utility implementation of an SBA that rejects all inputs, i.e., which describes the empty language.
EmptySPA<I>	A utility implementation of an SPA that rejects all inputs, i.e., describes the empty language.
EmptySPMM<I,O>	A utility implementation of an SPMM that transduces all input words to a sequence of the given erroneous output symbol.
EnumAlphabet<E extends Enum<E>>
FastAlphabet<I extends MutableNumericID>	A fast alphabet implementation, that assumes identifiers are stored directly in the input symbols.
FastDFA<I>
FastDFAState
FastMealy<I,O>	A fast implementation of a Mealy machine.
FastMealyState<O>	A state in a FastMealy automaton.
FastMoore<I,O>	A fast implementation of a Moore automaton.
FastMooreState<O>	A state in a FastMoore automaton.
FastNFA<I>
FastNFAState
FastPowersetDTS<S extends NumericID,I,T>
FastPowersetState<S>
FastProbMealy<I,O>
FastProbMealyState<O>
GrowingMapAlphabet<I>	An extension of the MapAlphabet that also allows adding new symbol after construction.
GrowingVPAlphabet<I>	A VPAlphabet implementation that allows to add new symbols after its construction.
ListAlphabet<I>
Location	Location type used for the default 1-SEVPA.
MapAlphabet<I>	A map-based alphabet implementation, that does not impose any restriction on the input symbol class.
MealyLassoImpl<I,O>	A MealyLasso is a lasso for MealyMachines.
MealyTransition<S,O>	A transition of a mealy machine, comprising a successor state and an output symbol.
ModalEdgePropertyImpl
MTSTransition<TP extends MutableModalEdgeProperty>
PrettyVisualizationHelper<N,E>
ProceduralModalEdgePropertyImpl
SimpleMapGraph<N>	A very simple graph realization, where nodes can be arbitrary Java objects.
SingletonAlphabet<I>	A specialized implementation for Alphabets containing only a single symbol.
SizeDFAModelCheckerCache<I,P,R>	A DFAModelCheckerCache that invalidates the cached counter examples when ModelChecker.findCounterExample(Object, Collection, Object) is called with a DFA with a size different, and an input alphabet different from the previous call.
SizeDFAModelCheckerLassoCache<I,P>
SizeMealyModelCheckerCache<I,O,P,R>
SizeMealyModelCheckerLassoCache<I,O,P>
StackSBA<S,I>	A stack-based implementation for the (instrumented) language of an SBA.
StackSPA<S,I>	A stack-based implementation for the (instrumented) language of an SPA.
StackSPMM<S,I,T,O>	A stack-based implementation for the (instrumented) transductions of an SPMM.
StackState<S,I,P>	A stack-based state in a procedural system.
Symbol<I>
UniversalCompactDet<I,SP,TP>	A default implementation for AbstractCompactDeterministic that uses CompactTransition as transition type and supports various types of state and transition properties.
UniversalCompactSimpleDet<I,SP>	A AbstractCompactSimpleDeterministic-based implementation for automata that need to store generic state properties.
Visualization
VisualizationProvider
VPManager
VPSym<T>	Utility class used to wrap input symbols of a VPAlphabet.