All Classes

Class	Description
AbstractAlphabet<I>
AbstractAutomatonGraphView<S,A extends Automaton<S,?,?>,E>
AbstractBasicLinkedListEntry<E,T extends AbstractBasicLinkedListEntry<E,T>>	Abstract base class for entries in a linked list.
AbstractBinaryFormulaNode<L,AP>	Abstract super-class for binary (sub-) formulas.
AbstractBricsAutomaton	Base class for Brics automata adapters.
AbstractClassPathFileSource
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.
AbstractETFWriter<I,A extends Automaton<?,I,?>>	This class provides methods to write automata in LTSmin's ETF format.
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>
AbstractFixedPointFormulaNode<L,AP>	Abstract super-class for fix-point (sub-) formulas.
AbstractFormulaNode<L,AP>	Abstract super-class for (sub-) formulas.
AbstractFSM2MealyParser<I,O>	An FSM parser for Mealy machines.
AbstractFSMParser<I>	This class provides methods to parse automata in FSM format.
AbstractFSMParser.Part	An enumeration for the three parts in the FSM file.
AbstractIncrementalDFABuilder<I>	Abstract base class for IncrementalDFABuilders.
AbstractLasso<I,D>
AbstractLinkedList<E,T extends LinkedListEntry<E,T>>	Abstract base class for linked lists.
AbstractLowLevelAutomatonCopier<S1,I1,T1,S2,I2,T2,SP2,TP2,TS1 extends TransitionSystem<S1,? super I1,T1>>
AbstractLTSmin<I,A,R>	An LTL model checker using LTSmin.
AbstractLTSminLTL<I,A,L extends Lasso<I,?>>	An LTSmin model checker for full LTL.
AbstractLTSminLTLMealy<I,O>	An LTL model checker using LTSmin for Mealy machines.
AbstractLTSminMonitor<I,A,R>	An LTSmin model checker for monitors.
AbstractLTSminMonitorMealy<I,O>	A monitor model checker using LTSmin for Mealy machines.
AbstractModalFormulaNode<L,AP>	Abstract super-class for modal (sub-) formulas.
AbstractMutableNumericID
AbstractPrintable	Abstract base class for printables.
AbstractPropertyTransformer<T extends AbstractPropertyTransformer<T,L,AP>,L,AP>	Base class used to represent a property transformer, i.e., a function which maps a subset of formulas to a subset of formulas.
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.
AbstractSmartCollection<E>	This class eases the implementation of the SmartCollection interface.
AbstractSymbol<S extends AbstractSymbol<S>>
AbstractSystemPropertiesSource
AbstractThreeLevelIterator<L1,L2,L3,O>
AbstractTwoLevelIterator<L1,L2,O>
AbstractUnaryFormulaNode<L,AP>	Abstract super-class for unary (sub-) formulas.
AbstractUnfoldingModelChecker<I,A,P,L extends Lasso<I,?>>	An ModelCheckerLasso that can unfold loops of lassos.
AbstractVisualizationHelper<S,I,T,A extends Automaton<S,I,T>>	Abstract visualization helper for IncrementalDFABuilders.
AbstractVPAlphabet<I>	Abstract utility class that implements functionality shared across different subtypes.
Acceptance	Tri-state acceptance value.
AcceptanceCombiner
AcceptanceGraph<N,E>	Interface for finite graphs that embody the concept of node acceptance.
Acceptors
AcceptorTS<S,I>	A transition system whose semantics are defined by whether a state is "accepting" or not.
AdaptiveMealyBuilder<I,O>	A variation of the IncrementalMealyBuilder interface that allows one to override previously inserted traces.
AdaptiveMealyTreeBuilder<I,O>
ADDSolver<L,AP>	Implementation based on property transformers being represented by ADDs (Algebraic Decision Diagrams).
ADDTransformer<L,AP>	An ADDTransformer represents a property transformer for a single ADD (Algebraic Decision Diagram).
ADDTransformerSerializer<L,AP>	This class can be used to serialize and deserialize ADDTransformers.
ADS	General purpose facade for computing adaptive distinguishing sequences.
ADSLeafNode<S,I,O>	An ADS-specific implementation of a leaf node.
ADSNode<S,I,O>	A (simplified) node in an adaptive distinguishing sequence.
ADSSymbolNode<S,I,O>	An ADS-specific implementation of a symbol node.
ADSUtil	Utility class, that offers some operations revolving around adaptive distinguishing sequences.
AFNode<L,AP>	Java representation of a "AF" (sub-)formula.
AggregateDOTVisualizationHelper<N,E>
AggregateVisualizationHelper<N,E>
AGNode<L,AP>	Java representation of a "AG" (sub-)formula.
AllDefinedInputsIterator<S,I>
AllUndefinedInputsIterator<S,I>
Alphabet<I>	Class implementing an (indexed) alphabet.
Alphabets	Utility methods concerning alphabets.
AndNode<L,AP>	Java representation of a "&&" (sub-)formula.
APSPResult<N,E>	Result interface for the all pairs shortest paths problem.
ArrayAlphabet<I>
ArrayMapping<K extends NumericID,V>
ArrayStorage<T>	A thin wrapper around a simple Object[] array.
ArrayUtil	Utility methods for arrays.
ArrayWritable<T>	Unified interface for (collection) classes that allow writing their contents to an array.
AtomicNode<L,AP>	Java representation of an "atomic proposition" (sub-)formula.
ATRSequences<I>	A data class for aggregating access sequences, terminating sequences, and return sequences.
ATSequences<I>	A data class for aggregating access sequences and terminating sequences.
AUNode<L,AP>	Java representation of a "AU" (sub-)formula.
Automata
AutomataLibLocalPropertiesSource
AutomataLibPropertiesSource
AutomataLibProperty	An enum of all the system properties currently used by AutomataLib.
AutomataLibSettings
AutomataLibSettingsSource
AutomataLibSystemPropertiesSource
Automaton<S,I,T>	Basic interface for an automaton.
AutomatonBuilder<S,I,T,SP,TP,A extends MutableAutomaton<S,? super I,T,? super SP,? super TP>>
AutomatonBuilders	Fluent interface automaton builders.
AutomatonCopyMethod
AutomatonCreator<A,I>
AutomatonGraphView<S,I,T,A extends Automaton<S,I,T>>
AutomatonInitialPartitioning	This enum allows to conveniently specify how the states of a deterministic automaton are initially partitioned when initializing the partition refinement data structure.
AutomatonLowLevelCopy
AutomatonType
AutomatonVisualizationHelper<S,I,T,A extends Automaton<S,I,T>>
AUTParser	A parser for automata specified in the AUT format (see http://cadp.inria.fr/man/aut.html for further information).
AUTSerializationProvider
AUTWriter	A utility class that exports automata to the AUT format (see http://cadp.inria.fr/man/aut.html for further information).
AWUNode<L,AP>	Java representation of an "AWU" (sub-)formula.
AWUtil	Utility class for writing containers to arrays.
BackedGeneralPriorityQueue<E,K extends Comparable<K>>	A SmartGeneralPriorityQueue implementation that is backed by a SmartDynamicPriorityQueue.
BackedGeneralPriorityQueue.Entry<E,K extends Comparable<K>>	Note: this class has a natural ordering that is inconsistent with equals.
BacktrackingSearch	A class containing methods for computing adaptive distinguishing sequences (for arbitrary sets of states) by means of a backtracking approach.
BacktrackingSearch.CostAggregator	Utility enum, that allows to specify the optimization criterion when performing and optimal ADS search.
BDDSolver<L,AP>	Implementation based on property transformers being represented by BDDs (Binary Decision Diagrams).
BDDTransformer<L,AP>	A BDDTransformer represents a property transformer for a list of BDDs (Binary Decision Diagrams), one per subformula.
BDDTransformerSerializer<L,AP>	This class can be used to serialize and deserialize BDDTransformers.
BidirectionalGraph<N,E>	Interface for bidirectional graph.
BidirectionalGraph.IntAbstraction<E>	Interface for node integer abstractions of a BidirectionalGraph.
BiIntFunction<R>	An int-primitive version of the BiFunction.
BinaryHeap<E>	A PriorityQueue implementation using a binary heap.
Bisimulation
BitSetIterator	Iterator for iterating over a BitSet like over a normal collection.
Block<S,L>	A block in the partition calculated during minimization.
Block	A block (i.e., partition class) that is maintained during the Paige/Tarjan partition refinement algorithm (see PaigeTarjan).
BlockAutomaton<S,L>	A "block automaton", i.e. an automaton-style representation of the minimization result in which each block forms a state.
BlockEdge<S,L>	An edge in a BlockAutomaton.
BlockMap<V>	Class for associating arbitrary values with the blocks of a minimization result.
BlockPropertyDecoder<P>
BlockPropertyEncoder<P>
BoxNode<L,AP>	Java representation of a "[]" (sub-)formula.
BricsDFA	Adapter class for wrapping a Brics automaton as a DFA.
BricsNFA	Adapter class for wrapping a Brics automaton as an NFA.
BricsTransitionProperty	The properties of an edge in a Brics automaton.
CapacityManagement	Control interface for collections supporting a capacity management, i.e., reserving space in advance in order to avoid repeated reallocations.
CFMPSGraphView<N,L,E,AP>	Graph representation of a ContextFreeModalProcessSystem that displays all nodes of its sub-procedures once, i.e., without incorporating execution semantics such as expansion.
CFMPSVisualizationHelper<N,L,E>
CharacterizingSets	Operations for calculating characterizing sets.
CharRange
CharRangeIterator
CharStringRange
CharStringRangeIterator
CmpUtil	Various methods for dealing with the comparison of objects.
CollectionsUtil	Various methods for operating on collections.
ColorVisualizationHelper	A VisualizationHelper for WitnessTrees that emphasizes nodes and edges of the witness and de-emphasizes the remaining ones.
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>
ConflictException	Conflict exception.
ContextFreeModalProcessSystem<L,AP>	Represents a Context-Free Modal Transition System as defined in the paper M3C: Modal Meta Model Checking.
Covers
CTLToMuCalc<L,AP>	A visitor that transforms a given CTL formula to an equivalent mu-calculus formula.
DefaultCFMPS<L,AP>
DefaultDOTVisualizationHelper<N,E>
DefaultLinkedList<E>	A simple linked list implementation that allows storing arbitrary elements.
DefaultLinkedListEntry<E>	The default linked list entry.
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.
DefaultVisualizationHelper<N,E>
DefaultVPAlphabet<I>	An alphabet-based, fixed size implementation of a VPAlphabet.
DefinedInputsIterator<S,I>
DependencyGraph<L,AP>	A dependency graph is used to represent a hierarchical equational system.
DeterministicAbstractions	Default implementations for DeterministicAutomaton abstractions.
DeterministicAbstractions.FullIntAbstraction<I,T,A extends DeterministicAutomaton.StateIntAbstraction<I,T>>
DeterministicAbstractions.StateIntAbstraction<S,I,T,A extends DeterministicAutomaton<S,I,T>>
DeterministicAcceptorTS<S,I>	A deterministic acceptor transition system.
DeterministicAutomaton<S,I,T>	Basic interface for a deterministic automaton.
DeterministicAutomaton.FullIntAbstraction<T>	Interface for full integer abstractions of a DeterministicAutomaton.
DeterministicAutomaton.IntAbstraction<T>	Base interface for integer abstractions of a DeterministicAutomaton.
DeterministicAutomaton.StateIntAbstraction<I,T>	Interface for state integer abstractions of a DeterministicAutomaton.
DeterministicEquivalenceTest
DeterministicOutputTS<S,I,T,O>
DeterministicPowersetView<S,I,T>
DeterministicStateOutputTS<S,I,T,O>
DeterministicTransitionOutputTS<S,I,T,O>
DeterministicTransitionSystem<S,I,T>	Deterministic transition system.
DetOutputAutomaton<S,I,T,D>	An automaton which deterministically produces an output for an input word.
DetSuffixOutputAutomaton<S,I,T,D>
DFA<S,I>	Deterministic finite state acceptor.
DFA2ETFWriter<I>	Write a DFA to ETF.
DFABuilder<S,I,A extends MutableDFA<S,? super I>>
DFALassoImpl<I>	A DFALasso is a lasso for DFAs.
DFAs	Operations on DFAs.
DFRecord<S,I,T,D>
DFRecord.LastTransition<S,I,T,D>
DiamondNode<L,AP>	Java representation of a "<>" (sub-)formula.
DiamondOperation<AP>	Implementation of the diamond function.
DiamondOperationDeadlock<AP>	Implementation of the diamond function when the node has exactly one successor.
DijkstraSSSP<N,E>	Implementation of Dijkstras algorithm for the single-source shortest path problem.
DirectPowersetDTS<S,I,T>
DOT	Utility class to simplify operating the GraphVIZ "dot" utility.
DOTGraphParser<NP,EP,G extends MutableGraph<?,?,NP,EP>>	General-purpose DOT parser for MutableGraphs.
DOTInputModelData<S,I,M extends SimpleTS<S,I>>	A utility data class, that extends InputModelData by labeling information of the model's states.
DOTInputModelDeserializer<S,I,M extends SimpleTS<S,I>>	A specialization of the InputModelDeserializer that returns a DOTInputModelData object which holds additional information about the state labels of the de-serialized automaton.
DOTMutableAutomatonParser<S,I,SP,TP,A extends MutableAutomaton<S,I,?,SP,TP>>	General-purpose DOT parser for MutableAutomatons.
DOTParsers	An aggregation of factory methods for obtaining DOT parsers for several types of automata / graphs.
DOTSerializationProvider<N,E>
DOTVisualizationHelper<N,E>	Extension to the VisualizationHelper interface for DOT specific methods.
DTSComposition<S1,S2,I,T1,T2,TS1 extends DeterministicTransitionSystem<S1,I,T1>,TS2 extends DeterministicTransitionSystem<S2,I,T2>>
DummyVP
DynamicIncrementalMealyTreeBuilder<I,O>	A variation of the normal IncrementalMealyTreeBuilder which stores the successor information of each tree-node in a dynamically allocated Map.
DynamicList<T extends MutableNumericID>
Edge	A utility class to aggregate information of an edge of a DOT graph.
EdgeLabels<E,L>	Edge label context, for Graphs with labeled edges.
EdgeVisualizationHelper	A VisualizationHelper for WitnessTrees that emphasizes edges of the witness and de-emphasizes the remaining ones.
EdgeWeights<E>	Edge weights concepts.
EFNode<L,AP>	Java representation of a "EF" (sub-)formula.
EGNode<L,AP>	Java representation of a "EG" (sub-)formula.
ElementReference	Marker interface for element reference.
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>>
EquationalBlock<L,AP>	Represents an equational block that aggregates its reference formula nodes.
EUNode<L,AP>	Java representation of a "EU" (sub-)formula.
EWUNode<L,AP>	Java representation of a "EWU" (sub-)formula.
FalseNode<L,AP>	Java representation of a "false" (sub-)formula.
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>
FinalNode<N>
FiniteAlphabetAutomaton<S,I,T>
FiniteKripkeStructure<N,E,AP>	A Kripke structure is a graph which has sets of atomic properties assigned to its nodes.
FiniteKTS<S,I,T,AP>	A finite Kripke Transition System combines the properties of a finite transition system and a KripkeInterpretation.
FiniteLabeledGraph<N,E,L>
FiniteRepresentation	This interface marks automata types that have a finite representation, i.e. can be represented by a finite number of entities.
FiniteStateAcceptor<S,I>	FiniteStateAcceptors accept regular languages.
FiniteStateAcceptor.FSAGraphView<S,I,A extends FiniteStateAcceptor<S,I>>
FloydWarshallAPSP<N,E>	Implementation of the Floyd-Warshall dynamic programming algorithm for the all pairs shortest paths problem.
FormatException
FormulaNode<L,AP>	Generic interface for formulas return by M3CParsers.
FormulaNodeVisitor<T,L,AP>
FSABuilder<S,I,A extends MutableFSA<S,? super I>>
FSAVisualizationHelper<S,I>
FSM2DFAParser<I>	Parses an FSM to a DFA.
FSM2MealyParserAlternating<I,O>	Parses a Mealy machine with alternating edge semantics from an FSM source.
FSM2MealyParserIO<I,O>	Parse a Mealy machine from an FSM source, with straightforward edge semantics.
FSMFormatException	Exception that may be thrown whenever an FSM is illegal.
FunctionsUtil	This class provides utility methods for Java 8 Function objects (and for the corresponding primitive specializations).
GfpNode<L,AP>	Java representation of a "nu" (sub-)formula.
Graph<N,E>	Graph interface.
Graph.IntAbstraction<E>	Interface for node integer abstractions of a Graph.
GraphCopy
GraphDOT	Methods for rendering a Graph or Automaton in the GraphVIZ DOT format.
Graphs
GraphTraversal
GraphTraversalAction	The type of GraphTraversalAction to be performed.
GraphTraversalVisitor<N,E,D>	Visitor interface for graph traversals.
GraphViewable
GraphVizBrowserVisualizationProvider
GraphVizSwingVisualizationProvider
GrowingAlphabet<I>	Alphabet class that supports adding new symbols.
GrowingAlphabetNotSupportedException	An exception to be thrown when functionality revolving around GrowingAlphabet.addSymbol(Object) is accessed (e.g. by trying to add an alphabet symbol to an automaton) but the given data structure was not properly set up (e.g.
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.
Holder<T>
HopcroftMinimization	Versions of Hopcroft's minimization algorithm for deterministic finite automata.
HopcroftMinimization.PruningMode	Allows for controlling how automata are pruned during minimization.
HTMLVisualizationHelper	A VisualizationHelper for WitnessTrees that renders the node labels as an HTML-based table.
IDChangeListener<T extends NumericID>
IDChangeNotifier<T extends NumericID>
IllegalConjunctionException
IncrementalConstruction<A,I>	Basic interface for incremental automata constructions.
IncrementalDFABuilder<I>	General interface for incremental DFA builders.
IncrementalDFADAGBuilder<I>	Incrementally builds an (acyclic) DFA, from a set of positive and negative words.
IncrementalDFATreeBuilder<I>	Incrementally builds a tree, from a set of positive and negative words.
IncrementalMealyBuilder<I,O>	General interface for incremental Mealy builders.
IncrementalMealyDAGBuilder<I,O>	Incrementally builds an (acyclic) Mealy machine, from a set of input and corresponding output words.
IncrementalMealyTreeBuilder<I,O>	Incrementally builds a tree with transition outputs from a set of input and corresponding output words.
IncrementalMooreBuilder<I,O>	General interface for incremental Moore builders.
IncrementalMooreDAGBuilder<I,O>	Incrementally builds an (acyclic) Moore machine from a set of input and corresponding output words.
IncrementalMooreTreeBuilder<I,O>	Incrementally builds a (tree-based) Moore machine from a set of input and corresponding output words.
IncrementalPCDFADAGBuilder<I>	The prefix-closed version of IncrementalDFADAGBuilder.
IncrementalPCDFATreeBuilder<I>	The prefix-closed version of IncrementalDFATreeBuilder.
IncrementalWMethodTestsIterator<I>	An iterator that enumerates the test cases as obtained through the W method conformance test in an incremental fashion.
IndefiniteGraph<N,E>	Interface for an (indefinite) graph structure.
IndefiniteSimpleGraph<N>	A simplified interface for indefinite graphs, exposing only adjacency information, but no further information about edge objects.
InitialNode<N>	Initial node concept.
InputAlphabetHolder<I>
InputModelData<I,M extends SimpleTS<?,I>>	A utility data class, that allows to pair a model that can react to input symbols with a corresponding alphabet.
InputModelDeserializer<I,M extends SimpleTS<?,I>>	A refinement of the ModelDeserializer interface for arbitrary models that can react to inputs.
InputModelSerializationProvider<I,OUT extends SimpleTS<?,I>,IN extends SimpleTS<?,I>>	A utility interface that unions InputModelSerializer and InputModelDeserializer and extends SerializationProvider.
InputModelSerializer<I,M extends SimpleTS<?,I>>	A refinement of the ModelSerializer interface for arbitrary models that can react to inputs.
IntDisjointSets	Interface for disjoint-set forest implementations that operate on a universe of contiguous integers.
IntRange
IntRangeIterator
IntrusiveLinkedList<T extends LinkedListEntry<T,T>>	An intrusive version of a linked list.
IntSeq	An IntSeq is an abstract read-only view on a finite, random-access data-structure for primitive integer values.
InvalidReferenceException	Exception that is thrown if an invalid ElementReference is used.
IOUtil	Utility methods for operating with java.io.* classes.
JungGraphVisualizationProvider
JungGraphVisualizationProvider.EdgeVisualization
JungGraphVisualizationProvider.NodeVisualization
JVMUtil	Utility class for Java/JVM specific utilities.
KripkeInterpretation<N,AP>	A Kripke interpretation for a graph.
Lasso<I,D>	A lasso is a single infinite word.
Lasso.DFALasso<I>	A DFALasso is a lasso for DFAs.
Lasso.MealyLasso<I,O>	A MealyLasso is a lasso for MealyMachines.
LearnLibV2Serialization
LeeYannakakis	Algorithm of Lee and Yannakakis for computing adaptive distinguishing sequences (of length at most n^2) in O(n^2) time (where n denotes the number of states of the automaton).
LfpNode<L,AP>	Java representation of a "mu" (sub-)formula.
LibLoader	Utility (singleton) class to manage loading of native libraries.
LinkedListEntry<E,T extends LinkedListEntry<E,T>>	Basic interface for entries in a linked list.
ListAlphabet<I>
LoadLibraryException	Unified exception to signal that loading of a native library has failed.
LoadPolicy	Specifies in which order a library to be loaded is searched for.
LocalFileSource
Location	Location type used for the default 1-SEVPA.
LowLevelAutomatonCopier<S1,S2>
LTSmin<I,A,R>	An LTSmin model checker.
LTSminAlternating<I,O,R>	A model checker using LTSmin for Mealy machines using alternating edge semantics.
LTSminDFA<I,R>	A model checker using LTSmin for DFAs.
LTSminIO<I,O,R>	A model checker using LTSmin for Mealy machines using synchronous edge semantics.
LTSminLTLAlternating<I,O>	An LTL model checker using LTSmin for Mealy machines using alternating edge semantics.
LTSminLTLAlternatingBuilder<I,O>
LTSminLTLDFA<I>	An LTL model checker using LTSmin for DFAs.
LTSminLTLDFABuilder<I>
LTSminLTLIO<I,O>	An LTL model checker using LTSmin for Mealy machines using synchronous edge semantics.
LTSminLTLIOBuilder<I,O>
LTSminLTLParser	A parser that verifies the syntax of LTL formulae of LTSmin.
LTSminMealy<I,O,R>	A feature of this ModelChecker, is that one can remove particular output symbols from the given MealyMachine hypothesis.
LTSminMonitorAlternating<I,O>	A monitor model checker using LTSmin for Mealy machines using alternating edge semantics.
LTSminMonitorAlternatingBuilder<I,O>
LTSminMonitorDFA<I>	A monitor model checker using LTSmin for DFAs.
LTSminMonitorDFABuilder<I>
LTSminMonitorIO<I,O>	A monitor model checker using LTSmin for Mealy machines using synchronous edge semantics.
LTSminMonitorIOBuilder<I,O>
LTSminUtil	A utility class that encapsulates certain technical aspects of LTSmin (e.g. accessibility of the binary, etc.)
LTSminVersion	A class for describing LTSmin version.
LYResult<S,I,O>	Utility class that holds some information aggregated during the ADS computation of LeeYannakakis.
M3CParser	This class can be used to parse formulas in CTL and the mu-calculus.
M3CSolver<F>	An interface for a generic M3C solver which may need to parse the given formula and thus may throw an exception when doing so.
M3CSolver.TypedM3CSolver<F>	A specialized M3CSolver which no longer throws a ParseException when solving a formula, but requires a type-safe formula object.
M3CSolvers	A factory for constructing M3CSolvers depending on the given ContextFreeModalProcessSystem.
MapAlphabet<I>	A map-based alphabet implementation, that does not impose any restriction on the input symbol class.
MapMapping<D,R>	Class that wraps a Mapping around a Map.
Mapping<D,R>	An interface for mapping objects of a certain domain type to objects of a certain range type.
Mappings	Collection of various methods dealing with Mappings.
Mealy2ETFWriterAlternating<I,O>	Write a Mealy machine with alternating edge semantics.
Mealy2ETFWriterIO<I,O>	Write a Mealy machine with straightforward IO semantics.
MealyBuilder<I,O>	A utility interface to share functionality between IncrementalMealyBuilders and AdaptiveMealyBuilders.
MealyBuilder<S,I,T,O,A extends MutableMealyMachine<S,? super I,T,? super O>>
MealyFilter	Various utility methods to filter Mealy machines.
MealyLassoImpl<I,O>	A MealyLasso is a lasso for MealyMachines.
MealyMachine<S,I,T,O>
MealyMachine.MealyGraphView<S,I,T,O,A extends MealyMachine<S,I,T,O>>
MealyMachines
MealyTransition<S,O>	A transition of a mealy machine, comprising a successor state and an output symbol.
MealyTransitionSystem<S,I,T,O>
MealyVisualizationHelper<S,I,T,O>
MinimizationResult<S,L>	The result structure of a minimization process.
Minimizer<S,L>	Automaton minimizer.
ModalEdgeProperty
ModalEdgeProperty.ModalType
ModalEdgePropertyImpl
ModalRefinement
ModalTransitionSystem<S,I,T,TP extends ModalEdgeProperty>	A modal transition system is a UniversalAutomaton in which transitions can be marked as may or must edges.
ModalTransitionSystem.MTSGraphView<S,I,T,TP extends ModalEdgeProperty,M extends ModalTransitionSystem<S,I,T,TP>>
ModelChecker<I,A,P,R>	A model-checker checks whether a given automaton satisfies a given property.
ModelChecker.DFAModelChecker<I,P,R>
ModelChecker.MealyModelChecker<I,O,P,R>	A model checker for Mealy machines.
ModelCheckerCache<I,A,P,R>	A model checker that caches calls to ModelChecker.findCounterExample(Object, Collection, Object).
ModelCheckerCache.DFAModelCheckerCache<I,P,R>
ModelCheckerCache.MealyModelCheckerCache<I,O,P,R>
ModelCheckerLasso<I,A,P,R extends Lasso<I,?>>	A model checker where the counterexample is a lasso.
ModelCheckerLasso.DFAModelCheckerLasso<I,P>
ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>
ModelCheckerLassoCache<I,A,P,R extends Lasso<I,?>>
ModelCheckerLassoCache.DFAModelCheckerLassoCache<I,P>
ModelCheckerLassoCache.MealyModelCheckerLassoCache<I,O,P>
ModelCheckingException	An Exception that may occur during model checking.
ModelDeserializer<M>	A generic interface for formalizing an arbitrary deserializer for a given model type.
ModelSerializer<M>	A generic interface for formalizing an arbitrary serializer for a given model type.
MooreBuilder<S,I,T,O,A extends MutableMooreMachine<S,? super I,T,? super O>>
MooreBuilderImpl<S,I,T,O,A extends MutableMooreMachine<S,? super I,T,? super O>>
MooreMachine<S,I,T,O>
MooreMachine.MooreGraphView<S,I,T,O,A extends MooreMachine<S,I,T,O>>
MooreTransitionSystem<S,I,T,O>
MooreVisualizationHelper<S,I,T,O>
MTSs	Operations on ModalTransitionSystems.
MTSTransition<TP extends MutableModalEdgeProperty>
MTSVisualizationHelper<S,I,T,TP extends ModalEdgeProperty,M extends ModalTransitionSystem<S,I,T,TP>>
MutableAutomaton<S,I,T,SP,TP>	A mutable automaton.
MutableDeterministic<S,I,T,SP,TP>	Interface for a mutable deterministic automaton.
MutableDeterministic.FullIntAbstraction<T,SP,TP>	Interface for full integer abstractions of a MutableDeterministic.
MutableDeterministic.IntAbstraction<T,SP,TP>	Base interface for integer abstractions of a MutableDeterministic.
MutableDeterministic.StateIntAbstraction<I,T,SP,TP>	Interface for state integer abstractions of a MutableDeterministic.
MutableDeterministicAbstraction	Default implementations for MutableDeterministic abstractions.
MutableDeterministicAbstraction.FullIntAbstraction<I,T,SP,TP,A extends MutableDeterministic.StateIntAbstraction<I,T,SP,TP>>
MutableDeterministicAbstraction.StateIntAbstraction<S,I,T,SP,TP,A extends MutableDeterministic<S,I,T,SP,TP>>
MutableDFA<S,I>
MutableDFAs
MutableEdgeLabels<E,L>
MutableFSA<S,I>
MutableGraph<N,E,NP,EP>	A graph that allows modification.
MutableGraph.IntAbstraction<E,NP,EP>	Interface for node integer abstractions of a MutableGraph.
MutableKripkeInterpretation<N,AP>
MutableMapping<D,R>	Mutable version of a Mapping, which supports setting keys for given values.
MutableMealyMachine<S,I,T,O>
MutableMealyMachines
MutableModalEdgeProperty
MutableModalTransitionSystem<S,I,T,TP extends MutableModalEdgeProperty>	A mutable version of ModalTransitionSystem that allows to add states and transitions.
MutableMooreMachine<S,I,T,O>
MutableNFA<S,I>
MutableNumericID
MutableProbabilistic<T>
MutableProbabilisticMealy<S,I,T,O>
MutableProceduralModalEdgeProperty
MutableProceduralModalProcessGraph<N,L,E,AP,TP extends MutableProceduralModalEdgeProperty>	A mutable version of the ProceduralModalProcessGraph.
MutableStateOutput<S,O>
MutableSubsequentialTransducer<S,I,T,O>	A mutable extension of a SubsequentialTransducer.
MutableTransitionOutput<T,O>
MutableUniversalBidirectionalGraph<N,E,NP,EP>
NearLinearEquivalenceTest
NFA<S,I>	Nondeterministic finite state acceptor.
NFAs	Operations on NFAs.
NNFVisitor<L,AP>	A visitor that transforms a given mu-calculus or CTL formula to negation-normal-form.
Node	A utility class to aggregate information of a node of a DOT graph.
NodeAcceptance<N>	Node acceptance concept, for Graphs that represent a structure for deciding acceptance or rejection.
NodeIDs<N>	An interface for translating between graph nodes and their primitive representations as integers.
NodeVisualizationHelper	A VisualizationHelper for WitnessTrees that emphasizes nodes of the witness and de-emphasizes the remaining ones.
NonClosingInputStream	A delegating input stream that does nothing when being closed.
NonClosingOutputStream	A delegating output stream that does not close but flush the delegate output stream.
NotNode<L,AP>	Java representation of a "!"
NumericID
OneSEVPA<L,I>	A specialized interface for 1-SEVPAs (1-module single entry visibly push-down automata).
OneSEVPAMinimizer	A Paige/Tarjan partition refinement based minimizer for OneSEVPAs.
OneSEVPAs	Operations on OneSEVPAs.
OrNode<L,AP>	Java representation of a "||" (sub-)formula.
Output<I,D>	Feature for automata that compute an output.
OutputAutomaton<S,I,T,D>
PaigeTarjan	An implementation of the Paige/Tarjan partition refinement algorithm.
PaigeTarjan.WorklistPolicy	Determines how the worklist is managed, i.e., where newly created blocks are inserted.
PaigeTarjanExtractors	This class provides methods for translating the result of a PaigeTarjan coarsest stable partition computation into several common, more usable forms such as automata.
PaigeTarjanInitializers	This class provides several methods to initialize a PaigeTarjan partition refinement data structure from common sources, e.g., automata.
PaigeTarjanMinimization	A utility class that offers shorthand methods for minimizing automata using the partition refinement approach of PaigeTarjan.
Pair<T1,T2>	Immutable pair class.
ParseException	This exception is thrown when parse errors are encountered.
ParseException	This exception is thrown when parse errors are encountered.
ParseException	This exception is thrown when parse errors are encountered.
ParseException	This exception is thrown when parse errors are encountered.
Path<N,E>
PlatformProperties
PMPGVisualizationHelper<N,E,AP>
PositiveIntSet	A Set for positive ints that internally stores its elements in a BitSet.
PowersetViewTS<S,I,T,OS,OT>
PrettyVisualizationHelper<N,E>
Printable	Interface that allows outputting to an Appendable (e.g., a StringBuilder) instead of simply using Object.toString().
PrintStreamDiagnosticListener
Probabilistic<T>
ProbabilisticMealyMachine<S,I,T,O>
ProbabilisticOutput<O>
ProceduralGraphView<S,I>	Graph representation of a ProceduralSystem that displays all states of its sub-procedures once, i.e., without incorporating execution semantics such as stack contents.
ProceduralInputAlphabet<I>	A specialized version of a VPAlphabet that is tailored towards procedural systems.
ProceduralModalEdgeProperty
ProceduralModalEdgeProperty.ProceduralType
ProceduralModalEdgePropertyImpl
ProceduralModalProcessGraph<N,L,E,AP,TP extends ProceduralModalEdgeProperty>	Represents a Procedural Modal Transition System as defined in the paper M3C: Modal Meta Model Checking.
ProceduralOutputAlphabet<O>	A specialized Alphabet for procedural systems that combines a regular output alphabet with a designated error symbol.
ProceduralVisualizationHelper<S,I>	Default VisualizationHelper for procedural systems.
ProcessUtil	Utility class for invoking system processes.
ProductOneSEVPA<L1,L2,I>	Production automaton that allows to join two given OneSEVPAs.
PropertyEdgeWeights<E>
RandomAutomata
RandomAutomatonGenerator<S,I,T,SP,TP,A extends MutableAutomaton<S,I,T,SP,TP>>
RandomDeterministicAutomatonGenerator<S,I,T,SP,TP,A extends MutableDeterministic<S,I,T,SP,TP>>
RandomICAutomatonGenerator<SP,TP>	A random generator for initially connected (IC) deterministic automata.
RandomUtil
RecursiveADSNode<S,I,O,N extends RecursiveADSNode<S,I,O,N>>	An interface representing a node in an adaptive distinguishing sequence (which essentially forms a decision tree).
Ref<T>	An abstraction for (weak or strong) references.
ReflectUtil	Utility methods for using Java reflection.
ReflexiveMapView<T>	An immutable, reflexive Map view for a given set of elements.
Refs	Utility functions for dealing with references.
ResizingArrayStorage<T>	Class that provides a resizable array storage of a certain type.
ReusableIterator<T>	A utility class that allows to reuse an Iterator.
SAFOutput	Serializer for the SAF (simple automaton format).
SAFSerializationDFA
SAFSerializationNFA
SBA<S,I>	A system of behavioral automata.
SBAs	Operations on SBAs.
SBAWMethodTestsIterator<I>	A conformance test iterator for SBAs that is based on the W-method.
ScalingThreadPoolExecutor	A ThreadPoolExecutor that internally uses a ScalingThreadPoolExecutor.ScalingLinkedBlockingQueue to manage scheduled tasks.
SCCCollector<N>
SCCListener<N>
SCCs	Algorithms for finding strongly-connected components (SCCs) in a graph.
SerializationProvider<OUT,IN>	A utility interface that unions ModelSerializer and ModelDeserializer.
SettingsSource
SEVPA<L,I>	Interface for k-SEVPAs (k-module single entry visibly push-down automata), a visibly push-down automaton of specific structure and semantics.
SEVPAGraphView<L,I>
SEVPAGraphView.SevpaViewEdge<S,I>
ShortestPaths	Unweighted shortest path search in graphs.
ShrinkableAutomaton<S,I,T,SP,TP>	A mutable automaton that also supports destructive modifications, i.e., removal of states and transitions.
ShrinkableDeterministic<S,I,T,SP,TP>	A mutable deterministic automaton that also supports destructive operations, i.e., removal of states and transitions.
ShrinkableGraph<N,E>	A graph that supports (desirably efficient) removal of nodes and edges.
SimpleAutomaton<S,I>	A simple automaton, i.e., a SimpleTS with a finite number of states.
SimpleAutomatonDeserializer<S,I>	A refining interface of InputModelDeserializer that binds the model to SimpleAutomatons.
SimpleAutomatonSerializationProvider<S,I>	A utility interface that unions SimpleAutomatonSerializer and SimpleAutomatonDeserializer.
SimpleAutomatonSerializer<I>	A refining interface of InputModelSerializer that binds the model to SimpleAutomatons.
SimpleDeterministicAbstractions	Default implementations for SimpleDeterministicAutomaton abstractions.
SimpleDeterministicAbstractions.FullIntAbstraction<I,A extends SimpleDeterministicAutomaton.StateIntAbstraction<I>>	Base class implementing the default way of obtaining a SimpleDeterministicAbstractions.FullIntAbstraction, i.e., building on top of a SimpleDeterministicAbstractions.StateIntAbstraction and a mapping from integers to (concrete) input symbols.
SimpleDeterministicAbstractions.IntAbstraction<S,A extends SimpleDeterministicAutomaton<S,?>>	Base class implementing the default way of obtaining an integer abstraction from an automaton, i.e., by mapping states to integers and vice versa using the StateIDs mapping obtained via SimpleAutomaton.stateIDs().
SimpleDeterministicAbstractions.StateIntAbstraction<S,I,A extends SimpleDeterministicAutomaton<S,I>>	Base class implementing the default way of obtaining a SimpleDeterministicAutomaton.StateIntAbstraction.
SimpleDeterministicAutomaton<S,I>	A simple deterministic automaton.
SimpleDeterministicAutomaton.FullIntAbstraction	Interface for an integer abstraction that abstracts both states and input symbols to integers.
SimpleDeterministicAutomaton.IntAbstraction	Basic interface for integer abstractions of automata.
SimpleDeterministicAutomaton.StateIntAbstraction<I>	Interface for integer abstractions of an automaton that operate on non-abstracted input symbols (i.e., input symbols are of type I).
SimpleDTS<S,I>	A simple deterministic transition system.
SimpleGraph<N>	The finite version of a IndefiniteSimpleGraph.
SimpleGraph.IntAbstraction	Basic interface for integer abstractions of graphs.
SimpleMapGraph<N>	A very simple graph realization, where nodes can be arbitrary Java objects.
SimpleNodeIDs<N>
SimpleStateIDs<S>
SimpleTS<S,I>	A simple transition system.
SinglePropertyDecoder<P>
SinglePropertyEncoder<P>
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>
SmartCollection<E>	An extended collection interface.
SmartDeque<E>	A double-ended queue (deque), allowing access, removal and insertion of elements both at the beginning and the end.
SmartDynamicPriorityQueue<E>	A priority queue interface.
SmartGeneralPriorityQueue<E,K extends Comparable<K>>	A generalized priority queue which allows storing arbitrary elements that don't have to be comparable, neither by their natural ordering nor by a provided Comparator.
SmartPriorityQueue<E>	Priority queue interface.
SmartSequence<E>	Sequence interface.
SolverData<N,T extends AbstractPropertyTransformer<T,L,AP>,L,AP>	A class used to store ProceduralModalProcessGraph-specific data for the SolverHistory.
SolverHistory<T extends AbstractPropertyTransformer<T,L,AP>,L,AP>	A class used to store internal information produced by AbstractDDSolver.solveAndRecordHistory(net.automatalib.modelchecker.m3c.formula.FormulaNode<L, AP>) while checking the satisfiability of a formula.
SolverState<N,T extends AbstractPropertyTransformer<T,L,AP>,L,AP>	Stores internal information produced during the update of a node in AbstractDDSolver.
SPA<S,I>	A system of procedural automata.
SPAs	Operations on SPAs.
SPATestsIterator<I>	A conformance test iterator for SPAs that applies a given regular conformance test to each procedure of the SPA.
SPMM<S,I,T,O>	A system of procedural Mealy machines.
SPMMs	Operations on SPMMs.
SPMMWMethodTestsIterator<I,O>	A conformance test iterator for SPMMs that is based on the W-method.
SSSPResult<N,E>	Result interface for the single-source shortest path (SSSP) problem.
SSTVisualizationHelper<S,I,T,O>
StackContents	A simplified stack implementation that allows to store integer values.
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.
State<L>	Utility class to combine an entity (e.g. a location) with stack information.
StateAsNodeIDs<S>
StateEquivalence	A utility class for computing an adaptive distinguishing sequence by means of solving the state equivalence problems, i.e. computing and ADS for two states only.
StateIDGrowingMapping<S,V>
StateIDs<S>	An interface for translating between automaton states and their primitive representations as integers.
StateIDStaticMapping<S,V>
StateLocalInput<S,I>	Concept for transition systems, that can for each state return the set of input symbols for which successor states are defined.
StateLocalInputMealyMachine<S,I,T,O>
StateOutput<S,O>	State output concept.
StateOutputAutomaton<S,I,T,O>
StateSignature	Utility class for constructing state signatures used for classifying states during PaigeTarjanInitializers.
StringADDSolver	An ADD solver for generic, string-based formulas.
StringBDDSolver	A BDD solver for generic, string-based formulas.
StringIndexMapping	Class for transforming integer index values into string values (using latin characters, therefore effectively realizing a radix-26 representation of numbers).
StringSymbolMapper<AI>	A default implementation that maps abstract input symbol to their String representations while adding an incrementing number to mapped call symbols.
StringUtil	Miscellaneous utility functions for Strings.
StrongRef<T>	A strong reference wrapper, complying to the Ref interface.
SubsequentialTransducer<S,I,T,O>	A subsequential transducer (or SST) is an DeterministicOutputTS whose state and transition properties are output-words.
SubsequentialTransducer.SSTGraphView<S,I,T,O,A extends SubsequentialTransducer<S,I,T,O>>
SubsequentialTransducers	Utility methods of SubsequentialTransducers.
SuffixOutput<I,D>	Feature for automata that compute a suffix-observable output function, i.e., they compute an output containing a part that can be attributed to a suffix of the input.
SupportsGrowingAlphabet<I>	Interface for declaring that a data structure supports adding new alphabet symbols after its instantiation.
Symbol<I>
SymbolMapper<AI,CI>	An interface for mapping (abstract) SEVPA input symbols to concrete SPA input symbols.
TAFFormatException	Exception to signal fatal errors during parsing TAF inputs.
TAFParseDiagnosticListener	Diagnostic listener for non-fatal errors and warnings during parsing of a TAF file.
TAFParser	Facade for TAF parsing.
TAFSerializationDFA
TAFSerializationMealy
TAFWriter	This class provides methods to write automata in the TAF format.
TarjanSCCRecord
TarjanSCCVisitor<N,E>	Depth-first traversal visitor realizing Tarjan's algorithm for finding all strongly-connected components (SCCs) in a graph.
Transducers
TransformerSerializer<T extends AbstractPropertyTransformer<T,L,AP>,L,AP>	Utility interface for serializing AbstractPropertyTransformer implementations.
TransitionEdge<I,T>
TransitionEdge.Property<I,TP>
TransitionOutput<T,O>	Transition output concept.
TransitionOutputAutomaton<S,I,T,O>
TransitionPredicate<S,I,T>
TransitionPredicates
TransitionSystem<S,I,T>	Transition system interface.
TraversalOrder
Triple<T1,T2,T3>	Immutable triple class.
TrueNode<L,AP>	Java representation of a "true" (sub-)formula.
TS
TS.TransRef<S,I,T>
TSComposition<S1,S2,I,T1,T2,TS1 extends TransitionSystem<S1,I,T1>,TS2 extends TransitionSystem<S2,I,T2>>
TSCompositions
TSCopy
TSCopyVisitor<S1,I1,T1,S2,I2,T2,SP2,TP2>
TSTraversal
TSTraversalAction	The type of TSTraversalAction to be performed.
TSTraversalMethod
TSTraversalVisitor<S,I,T,D>	Visitor interface for transition system traversals.
TypedADDSolver<L,AP>	An ADD solver for strongly-typed formulas.
TypedBDDSolver<L,AP>	A BDD solver for strongly-typed formulas.
UnclosableInputStream	A delegating input stream that throws an exception when closed.
UnclosableOutputStream	A delegating output stream that throws an exception when closed.
UndefinedInputsIterator<S,I>
UndefinedPropertyAccessException	This specialized exception can be thrown if during the traversal of an automaton or transition system an undefined property (e.g. a state or a transition output) is accessed, that is otherwise required for returning a valid result.
UndirectedGraph<N,E>	An undirected graph.
UnionFind	The well-known disjoint-set forest data structure for dealing with partitions on a fixed-range integer domain.
UnionFindRemSP	Implementation of a disjoint set (union-find) data structure for integers, based on Rem's algorithm, as described in the paper Experiments on Union-Find Algorithms for the Disjoint-Set Data Structure (M.
UniversalAutomaton<S,I,T,SP,TP>	A universal automaton is a generalized representation of automata, with unified access to the properties of states and transitions.
UniversalAutomatonGraphView<S,I,T,SP,TP,A extends UniversalAutomaton<S,I,T,SP,TP>>
UniversalBidirectionalGraph<N,E,NP,EP>
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.
UniversalDeterministicAbstractions	Default implementations for UniversalDeterministicAutomaton abstractions.
UniversalDeterministicAbstractions.FullIntAbstraction<I,T,SP,TP,A extends UniversalDeterministicAutomaton.StateIntAbstraction<I,T,SP,TP>>
UniversalDeterministicAbstractions.StateIntAbstraction<S,I,T,SP,TP,A extends UniversalDeterministicAutomaton<S,I,T,SP,TP>>
UniversalDeterministicAutomaton<S,I,T,SP,TP>	A DeterministicAutomaton with state and transition properties.
UniversalDeterministicAutomaton.FullIntAbstraction<T,SP,TP>	Interface for full integer abstractions of a UniversalDeterministicAutomaton.
UniversalDeterministicAutomaton.IntAbstraction<T,SP,TP>	Base interface for integer abstractions of a UniversalDeterministicAutomaton.
UniversalDeterministicAutomaton.StateIntAbstraction<I,T,SP,TP>	Interface for state integer abstractions of a UniversalDeterministicAutomaton.
UniversalDTS<S,I,T,SP,TP>	Universal deterministic transition system.
UniversalFiniteAlphabetAutomaton<S,I,T,SP,TP>
UniversalGraph<N,E,NP,EP>
UniversalGraph.IntAbstraction<E,NP,EP>	Interface for node integer abstractions of a UniversalGraph.
UniversalIndefiniteGraph<N,E,NP,EP>	A universal graph, i.e., with (possibly empty) node and edge properties.
UniversalTransitionSystem<S,I,T,SP,TP>	A "universal" transition system, which captures the possibility to assign properties to states and transitions.
UnmodifiableListIterator<T>	Wraps a given ListIterator so that any mutating operations throw an UnsupportedOperationException.
UnorderedCollection<E>	This class implements a collection for storing objects in no particular order.
VariableNode<L,AP>	Java representation of an "X" (sub-)formula.
VisitedState	Enum to use for indicating if a node/state has been visited.
Visualization
VisualizationHelper<S,I,T,O>	A utility class for rendering IncrementalMealyBuilders.
VisualizationHelper<N,E>	Helper interface for providing additional styling properties for plotting graphs.
VisualizationHelper.CommonAttrs
VisualizationHelper.CommonStyles
VisualizationHelper.EdgeAttrs
VisualizationHelper.EdgeStyles
VisualizationHelper.MTSEdgeAttrs
VisualizationHelper.NodeAttrs
VisualizationHelper.NodeShapes
VisualizationHelper.NodeStyles
VisualizationProvider
VPAlphabet<I>	Alphabet definition for visible push-down automata.
VPAlphabet.SymbolType	Classifies an input symbol either as a call symbol, an internal symbol, or a return symbol.
VPManager
VPSym<T>	Utility class used to wrap input symbols of a VPAlphabet.
WeakRef<T>	A weak reference wrapper, complying to the Ref interface.
WeightedSupplier<T>	This class implements a Supplier that randomly delegates to one of several (sub-)suppliers.
WitnessTree<L,AP>	A tree-like Graph that represents the BFS-style exploration of the tableau generated by the WitnessTreeExtractor.
WitnessTreeState<N,L,E,AP>	A utility class that represents a current configuration (node property) in the WitnessTree.
WMethodTestsIterator<I>	Iterator that returns test words generated by the W method.
Word<I>	A word is an ordered sequence of symbols.
WordBuilder<I>	A class for dynamically building Words.
WorksetAlgorithm<T,R>
WorksetMappingAlgorithm<T,E,R>
Worksets
WpMethodTestsIterator<I>	Iterator that returns test words generated by the partial W method.
WrapperUtil