All Classes and Interfaces
Class
Description
Abstract base class for entries in a linked list.
Abstract super-class for binary (sub-) formulas.
Base class for Brics automata adapters.
Abstract super class for compact automata representations.
A utility class that encapsulates necessary information for performing an update of the stored automata data.
Abstract super class that refines
AbstractCompact for deterministic automata.An abstract base-implementation for
MutableModalTransitionSystems.Abstract super class that refines
AbstractCompactDeterministic for transition-property-less automata.Abstract super class that refines
AbstractCompact for transition-property-less automata.Base implementation of the model checker which supports different types of property transformers.
Basic functionality for
Location-based SEVPA implementations.This class provides methods to write automata in LTSmin's ETF format.
Shared functionality for (non-) deterministic mutable automata.
Abstract super-class for fix-point (sub-) formulas.
Abstract super-class for (sub-) formulas.
An FSM parser for Mealy machines.
This class provides methods to parse automata in FSM format.
An enumeration for the three parts in the FSM file.
Abstract base class for
IncrementalDFABuilders.Abstract base class for linked lists.
AbstractLowLevelAutomatonCopier<S1,I1,T1,S2,I2,T2,SP2,TP2,TS1 extends TransitionSystem<S1,? super I1,T1>>
An LTL model checker using LTSmin.
An LTSmin model checker for full LTL.
An LTL model checker using LTSmin for Mealy machines.
An LTSmin model checker for monitors.
A monitor model checker using LTSmin for Mealy machines.
Abstract super-class for modal (sub-) formulas.
Abstract base class for printables.
Base class used to represent a property transformer, i.e., a function which maps a subset of formulas to a subset of
formulas.
An abstract implementation of a leaf node, that may be used by other ADS-extending classes.
An abstract implementation of a symbol node, that may be used by other ADS-extending classes.
Abstract class for k-SEVPAs that implements functionality shared across different subtypes.
A simplified immutable iterator that only requires to implement the calculation of the next element.
This class eases the implementation of the
SmartCollection interface.Abstract super-class for unary (sub-) formulas.
An
ModelCheckerLasso that can unfold loops of lassos.Abstract visualization helper for
IncrementalDFABuilders.Abstract utility class that implements functionality shared across different subtypes.
Tri-state acceptance value.
Interface for finite graphs that embody the concept of node acceptance.
A (default)
AcceptorPowersetViewTS implementation that represents states of the original acceptor transition
system via Sets.A
PowersetViewTS refinement that additionally captures the semantics of AcceptorTSs.A transition system whose semantics are defined by whether a state is "accepting" or not.
A variation of the
IncrementalMealyBuilder interface that allows one to override previously inserted traces.Implementation based on property transformers being represented by ADDs (Algebraic Decision Diagrams).
An ADDTransformer represents a property transformer for a single ADD (Algebraic Decision Diagram).
This class can be used to serialize and deserialize
ADDTransformers.General purpose facade for computing adaptive distinguishing sequences.
An ADS-specific implementation of a leaf node.
A (simplified) node in an adaptive distinguishing sequence.
An ADS-specific implementation of a symbol node.
Utility class, that offers some operations revolving around adaptive distinguishing sequences.
Java representation of a "AF" (sub-)formula.
Java representation of a "AG" (sub-)formula.
Class implementing an (indexed) alphabet.
Utility methods concerning alphabets.
Java representation of a "&&" (sub-)formula.
Result interface for the all pairs shortest paths problem.
A type-safe wrapper around a simple
Object[] array.Utility methods for arrays.
Unified interface for (collection) classes that allow writing their contents to an array.
Java representation of an "atomic proposition" (sub-)formula.
A data class for aggregating access sequences, terminating sequences, and return sequences.
A data class for aggregating access sequences and terminating sequences.
Java representation of a "AU" (sub-)formula.
An enum of all the system properties currently used by AutomataLib.
Basic interface for an automaton.
Convenience interface that describes an automaton with finite syntactic and finite semantic state space.
A fluent builder for
automata.Fluent builders for automata.
This enum allows to conveniently specify how the states of a deterministic automaton are initially partitioned when
initializing the partition refinement data structure.
Facade for AUT parsing.
A writer that exports automata to the AUT format.
Java representation of an "AWU" (sub-)formula.
Utility class for writing containers to arrays.
A
SmartGeneralPriorityQueue implementation that is backed by a SmartDynamicPriorityQueue.Note: this class has a natural ordering that is inconsistent with equals.
A class containing methods for computing adaptive distinguishing sequences (for arbitrary sets of states) by means of
a backtracking approach.
Utility enum, that allows to specify the optimization criterion when performing and optimal ADS search.
Facade for BA parsing.
A writer that exports automata to the BA format.
Implementation based on property transformers being represented by BDDs (Binary Decision Diagrams).
A BDDTransformer represents a property transformer for a list of BDDs (Binary Decision Diagrams), one per subformula.
This class can be used to serialize and deserialize
BDDTransformers.Interface for bidirectional graph.
Interface for
node integer abstractions of a BidirectionalGraph.An int-primitive version of the
BiFunction.A
PriorityQueue implementation using a binary heap.Iterator for iterating over a BitSet like over a normal collection.
A block in the partition calculated during minimization.
A block (i.e., partition class) that is maintained during the Paige/Tarjan partition refinement algorithm (see
Hopcroft).Java representation of a "[]" (sub-)formula.
Adapter class for wrapping a Brics automaton as a
DFA.Adapter class for wrapping a Brics automaton as an
NFA.The properties of an edge in a Brics automaton.
Control interface for collections supporting a capacity management, i.e., reserving space in advance in order to
avoid repeated reallocations.
Graph representation of a
ContextFreeModalProcessSystem that displays all nodes of its sub-procedures once,
i.e., without incorporating execution semantics such as expansion.Operations for calculating characterizing sets.
Various methods for dealing with the comparison of objects.
Various methods for operating on
Collections.A
VisualizationHelper for WitnessTrees that emphasizes nodes and edges of the witness and
de-emphasizes the remaining ones.An edge in an
AbstractCompactUniversalBidiGraph.An edge in an
AbstractCompactUniversalGraph.A compact graph representation that only stores adjacency information.
Implements a
MutableMMLT by storing adjacency information in compact arrays.A simple automaton that only stores adjacency information.
A compact bi-directional graph representation that supports arbitrary edge properties.
A compact graph representation that supports arbitrary edge properties.
A compact implementation that supports generic transition outputs.
A compact bi-directional graph representation that supports arbitrary node properties and edge properties.
A compact graph representation that supports arbitrary node properties and edge properties.
Conflict exception.
Represents a Context-Free Modal Transition System as defined in the paper M3C: Modal Meta Model Checking.
A visitor that transforms a given CTL formula to an equivalent mu-calculus formula.
A simple linked list implementation that allows storing arbitrary elements.
The default linked list entry.
Default implementation for an
MMLTSemantics that wraps arbitrary MMLTs.Default implementation for n-SEVPAs.
Default implementation for 1-SEVPAs.
Default implementation of a
ProceduralInputAlphabet.Default implementation of a
ProceduralOutputAlphabet.An alphabet-based, fixed size implementation of a
VPAlphabet.A dependency graph is used to represent a hierarchical equational system.
Abstractions for
DeterministicAutomatons.Interface for
full integer abstractions of a
DeterministicAutomaton.DeterministicAbstractions.FullIntAbstractionImpl<I,T,A extends DeterministicAbstractions.StateIntAbstraction<I,T>>
Base interface for
integer abstractions of a
DeterministicAutomaton.Interface for
state integer abstractions of a
DeterministicAutomaton.An
AcceptorPowersetViewTS-specific refinement of DeterministicPowersetView.A deterministic acceptor transition system.
Basic interface for a deterministic automaton.
Convenience interface that describes an automaton with finite syntactic and finite semantic state space.
An interface for providing deterministic, finite-state semantics.
A deterministic output automaton is a
deterministic automaton that can produce
outputs.A deterministic output transition system is a
determinisitc transition system
that can produce outputs.A thin
PowersetViewTS wrapper that may be used if the given transition system already is deterministic.An interface for providing deterministic, infinite-state semantics.
A deterministic state output transition system is a
deterministic output transition system that produces outputs based on its
state outputs.A deterministic suffix output automaton is a
deterministic output automaton that
can produce suffix outputs.A deterministic suffix output transition system is a
deterministic output transition system that can produce
suffix outputs.A deterministic traceable transition system is a
deterministic suffix output transition system whose outputs are collected while
traversing the transition system.A deterministic transition output transition system is a
deterministic output transition system that produces outputs based on its
transition outputs.Deterministic transition system.
Deterministic finite state acceptor.
Write a DFA to ETF.
A fluent builder for
DFAs.A DFALasso is a lasso for
DFAs.Operations on
DFAs.Java representation of a "<>" (sub-)formula.
Implementation of the diamond function.
Implementation of the diamond function when the node has exactly one successor.
Implementation of Dijkstra's algorithm for the single-source shortest path problem, as described in A note on two problems in connexion with graphs.
Utility class to simplify operating the GraphVIZ "dot" utility.
DOTCFMPSParser<N,L,E,AP,TP extends MutableProceduralModalEdgeProperty,P extends MutableProceduralModalProcessGraph<N,L,E,AP,TP>>
Parses a DOT file that defines a
ContextFreeModalProcessSystem.General-purpose DOT parser for
MutableGraphs.A utility data class, that extends
InputModelData by labeling information of the model's states.A specialization of the
InputModelDeserializer that returns a DOTInputModelData object which holds
additional information about the state labels of the de-serialized automaton.Parses a DOT file that defines an
MMLT.General-purpose DOT parser for
MutableAutomatons.An aggregation of factory methods for obtaining DOT parsers for several types of automata / graphs.
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>>
A variation of the normal
IncrementalMealyTreeBuilder which stores the successor information of each
tree-node in a dynamically allocated Map.A utility class to aggregate information of an edge of a DOT graph.
Edge label context, for
Graphs with labeled edges.A
VisualizationHelper for WitnessTrees that emphasizes edges of the witness and de-emphasizes the
remaining ones.Edge weights concepts.
Java representation of a "EF" (sub-)formula.
Java representation of a "EG" (sub-)formula.
Marker interface for element reference.
A utility implementation of an
SBA that rejects all inputs, i.e., which describes the empty language.A utility implementation of an
SPA that rejects all inputs, i.e., describes the empty language.A utility implementation of an
SPMM that transduces all input words to a sequence of the given erroneous
output symbol.Represents an equational block that aggregates its reference formula nodes.
Java representation of a "EU" (sub-)formula.
Java representation of a "EWU" (sub-)formula.
Utility methods for
Exceptions.Java representation of a "false" (sub-)formula.
A fast alphabet implementation, that assumes identifiers are stored directly in the input symbols.
A fast implementation of a Mealy machine.
A state in a
FastMealy automaton.A fast implementation of a Moore automaton.
A state in a
FastMoore automaton.A Kripke structure is a graph which has sets of atomic properties assigned to its nodes.
A finite Kripke Transition System.
This interface marks automata types that have a finite representation, i.e. can be represented by a finite number of
entities.
An interface for providing non-deterministic, finite-state semantics.
FiniteStateAcceptors accept regular languages.Implementation of the Floyd-Warshall dynamic programming algorithm for the all pairs shortest paths problem, as
described in Algorithm 97: Shortest path.
An exception that may be thrown when encountering an invalid format while de-serializing entities such as automata
models or formulas.
Generic interface for formulas return by
M3CParsers.A fluent builder for
FiniteStateAcceptors.Parses an FSM to a DFA.
Parses a Mealy machine with alternating edge semantics from an FSM source.
Parse a Mealy machine from an FSM source with straightforward edge semantics (as compared to
FSM2MealyParserAlternating).This class provides utility methods for Java 8
Function objects (and for the corresponding primitive
specializations).Java representation of a "nu" (sub-)formula.
Graph interface.
Interface for
node integer abstractions of a Graph.The type of
GraphTraversalAction to be performed.Visitor interface for graph traversals.
Alphabet class that supports adding new symbols.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.An extension of the
MapAlphabet that also allows adding new symbol after construction.A
VPAlphabet implementation that allows to add new symbols after its construction.Utility class for hash-based datastructures.
A class that holds a value.
An implementation of Hopcroft's algorithm for computing the functional coarsest partition.
This class provides methods for translating the result of a
Hopcroft coarsest stable partition computation
into several common, more usable forms such as automata.This class provides several methods to initialize a
Hopcroft partition refinement data structure from common
sources, e.g., automata.Hopcroft's minimization algorithm for deterministic finite automata.
A
VisualizationHelper for WitnessTrees that renders the node labels as an HTML-based table.Basic interface for incremental automata constructions.
General interface for incremental DFA builders.
Incrementally builds an (acyclic) DFA, from a set of positive and negative words.
Incrementally builds a tree, from a set of positive and negative words.
General interface for incremental Mealy builders.
Incrementally builds an (acyclic) Mealy machine, from a set of input and corresponding output words.
Incrementally builds a tree with transition outputs from a set of input and corresponding output words.
General interface for incremental Moore builders.
Incrementally builds an (acyclic) Moore machine from a set of input and corresponding output words.
Incrementally builds a (tree-based) Moore machine from a set of input and corresponding output words.
The prefix-closed version of
IncrementalDFADAGBuilder.The prefix-closed version of
IncrementalDFATreeBuilder.An iterator that enumerates the test cases as obtained through the W method conformance test in an incremental
fashion.
Interface for an (indefinite) graph structure.
A simplified interface for indefinite graphs, exposing only adjacency information, but no further information about
edge objects.
Initial node concept.
The concept of providing a single (potentially undefined) initial state.
The concept of providing (potentially multiple) initial states.
A utility data class, that allows to pair a model that can react to input symbols with a corresponding alphabet.
A refinement of the
ModelDeserializer interface for arbitrary models that can react to inputs.A refinement of the
ModelSerializer interface for arbitrary models that can react to inputs.An input symbol that represents a direct action without any delay.
Interface for disjoint-set forest implementations that operate on a universe of contiguous integers.
An intrusive version of a linked list.
An
IntSeq is an abstract read-only view on a finite, random-access data-structure for primitive integer
values.Exception that is thrown if an invalid
ElementReference is used.Utility methods for operating with
java.io.* classes.Utility methods for
Iterables.Utility methods for
Iterators.A Kripke interpretation for a graph.
A Kripke Transition System combines the properties of a
TransitionSystem and a KripkeInterpretation.A randomized state cover test generator based on the concepts of mutation testing as described in the paper Learning from Faults: Mutation Testing in Active Automata
Learning by Bernhard K.
The specific method for generating combinations of states during exploration.
A randomized transition cover test generator based on the concepts of mutation testing as described in the paper Learning from Faults: Mutation Testing in Active Automata
Learning by Bernhard K.
Method by which the prefixes of test words should be generated.
The metric by which to optimize path selection.
A lasso is a single infinite word.
A DFALasso is a lasso for
DFAs.A MealyLasso is a lasso for
MealyMachines.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).
Java representation of a "mu" (sub-)formula.
Utility (singleton) class to manage loading of native libraries.
Basic interface for entries in a linked list.
Unified exception to signal that loading of a native library has failed.
Specifies in which order a library to be loaded is searched for.
Location type used for
AbstractDefaultSEVPA.An LTSmin model checker.
A model checker using LTSmin for Mealy machines using alternating edge semantics.
A model checker using LTSmin for DFAs.
A model checker using LTSmin for Mealy machines using synchronous edge semantics.
An LTL model checker using LTSmin for Mealy machines using alternating edge semantics.
A builder for constructing
LTSminLTLAlternating instances.An LTL model checker using LTSmin for DFAs.
A builder for constructing
LTSminLTLDFA instances.An LTL model checker using LTSmin for Mealy machines using synchronous edge semantics.
A builder for constructing
LTSminLTLIO instances.A parser that verifies the syntax of LTL formulae of LTSmin.
A feature of this
ModelChecker, is that one can remove particular output
symbols from the given MealyMachine hypothesis.A monitor model checker using LTSmin for Mealy machines using alternating edge semantics.
A builder for constructing
LTSminMonitorAlternating instances.A monitor model checker using LTSmin for DFAs.
A builder for constructing
LTSminMonitorDFA instances.A monitor model checker using LTSmin for Mealy machines using synchronous edge semantics.
A builder for constructing
LTSminMonitorIO instances.A utility class that encapsulates certain technical aspects of LTSmin (e.g. accessibility of the binary, etc.)
A record for describing LTSmin versions.
Utility class that holds some information aggregated during the ADS computation of
LeeYannakakis.A factory for constructing
ModelCheckers for ContextFreeModalProcessSystems.This class can be used to parse formulas in CTL and the mu-calculus.
An interface for a generic M3C solver which may need to parse the given formula and thus may throw an exception when
doing so.
A specialized
M3CSolver which no longer throws a FormatException when solving a formula, but
requires a type-safe formula object.A factory for constructing
M3CSolvers depending on the given ContextFreeModalProcessSystem.A map-based alphabet implementation, that does not impose any restriction on the input symbol class.
An interface for mapping objects of a certain domain type to objects of a certain range type.
Collection of various methods dealing with
Mappings.Parser for reading
NFAs from the NFA-explicit format.Writer for serializing
NFAs into the NFA-explicit format.Write a Mealy machine with alternating edge semantics.
Write a Mealy machine with straightforward IO semantics.
A utility interface to share functionality between
IncrementalMealyBuilders and
AdaptiveMealyBuilders.A fluent builder for
MealyMachines.Various utility methods to filter Mealy machines.
A MealyLasso is a lasso for
MealyMachines.A transition of a mealy machine, comprising a successor state and an output symbol.
The result structure of a minimization process.
Automaton minimizer.
Base type for a Mealy Machine with Local Timers (MMLT).
A graph-based view for
MMLTs that explicitly represents timeouts as transitions between locations if
possible.Provides various functions that are related MMLTs.
Defines the semantics of an MMLT.
A visualization helper for MMLTs which Allows edge coloring and explicit resets in transition labels for easier
inspection.
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>>
A model-checker checks whether a given model satisfies a given property.
A model checker for Mealy machines.
A model checker that caches calls to
ModelChecker.findCounterExample(Object, Collection, Object).A model checker where the counterexample is a lasso.
Combines the two concepts of
ModelCheckerCaches and ModelCheckerLassos.An Exception that may occur during model checking.
A generic interface for formalizing an arbitrary deserializer for a given model type.
A generic interface for formalizing an arbitrary serializer for a given model type.
A fluent builder for
MooreMachines.Operations on
ModalTransitionSystems.MTSVisualizationHelper<S,I,T,TP extends ModalEdgeProperty,M extends ModalTransitionSystem<S,I,T,TP>>
A mutable automaton.
Convenience interface that describes an automaton with finite syntactic and finite semantic state space.
Interface for a mutable deterministic automaton.
Convenience interface that describes an automaton with finite syntactic and finite semantic state space.
Abstractions for
MutableDeterministics.Interface for
full integer abstractions of a
MutableDeterministic.MutableDeterministicAbstractions.FullIntAbstractionImpl<I,T,SP,TP,A extends MutableDeterministicAbstractions.StateIntAbstraction<I,T,SP,TP>>
Base interface for
integer abstractions of a
MutableDeterministic.Interface for
state integer abstractions of a
MutableDeterministic.MutableDeterministicAbstractions.StateIntAbstractionImpl<S,I,T,SP,TP,A extends MutableDeterministic<S,I,T,SP,TP>>
A graph that allows modification.
Interface for
node integer abstractions of a MutableGraph.Mutable version of a
Mapping, which supports setting keys for given values.A mutable extension of
MMLT that allows for modifying transition structure and timers.A mutable version of
ModalTransitionSystem that allows to add states and transitions.A mutable version of the
ProceduralModalProcessGraph.A
mutable extension of a SubsequentialTransducer.Implements Hopcroft and Karp's equivalence test, as described in A linear
algorithm for testing equivalence of finite automata.
Nondeterministic finite state acceptor.
Operations on
NFAs.A visitor that transforms a given mu-calculus or CTL formula to negation-normal-form.
A utility class to aggregate information of a node of a DOT graph.
Node acceptance concept, for
Graphs that represent a structure for deciding acceptance or rejection.An interface for translating between graph nodes and their primitive representations as integers.
A
VisualizationHelper for WitnessTrees that emphasizes nodes of the witness and de-emphasizes the
remaining ones.A delegating input stream that does nothing when being closed.
A delegating output stream that does not close but flush the delegate output stream.
Java representation of a "!"
A specialized interface for 1-
SEVPAs.A Hopcroft-based minimizer for
OneSEVPAs.Operations on
OneSEVPAs.Java representation of a "||" (sub-)formula.
Feature for transition systems that compute an output.
An output automaton is a
finite state output transition system.An output transition system is a
transition system that can produce outputs.Immutable pair class.
A (default)
PowersetViewTS implementation that represents states and transitions of the original transition
system via Sets and Collections.A powerset view is a deterministic view on a (potentially) non-deterministic transition system.
Interface that allows outputting to an
Appendable (e.g., a StringBuilder) instead of simply using
Object.toString().Graph representation of a
ProceduralSystem that displays all states of its sub-procedures once, i.e., without
incorporating execution semantics such as stack contents.A specialized version of a
VPAlphabet that is tailored towards procedural systems.Represents a Procedural Modal Transition System as defined in the paper M3C: Modal Meta Model Checking.
A specialized
Alphabet for procedural systems that combines a regular output alphabet with a designated error
symbol.Default
VisualizationHelper for procedural systems.Utility class for invoking system processes.
Production automaton that allows to join two given
OneSEVPAs.Allows for controlling how automata are pruned during minimization.
A random generator for initially connected (IC) deterministic automata.
An interface representing a node in an adaptive distinguishing sequence (which essentially forms a decision tree).
Provides a reduced version of the semantics automaton of an MMLT.
An abstraction for (weak or strong) references.
Utility methods for using Java reflection.
An immutable, reflexive
Map view for a given set of elements.Utility functions for dealing with references.
A utility class that allows to reuse an
Iterator.Facade for SAF (simple automaton format) parsing.
Facade for SAF (simple automaton format) parsing.
A system of behavioral automata.
Operations on
SBAs.A
ThreadPoolExecutor that internally uses a ScalingThreadPoolExecutor.ScalingLinkedBlockingQueue to manage scheduled tasks.Algorithms for finding strongly-connected components (SCCs) in a graph.
An interface for providing non-deterministic, infinite-state semantics.
A utility interface that unions
ModelSerializer and ModelDeserializer.Utility interface to mark the source of a setting.
Interface for k-SEVPAs (k-module single entry visibly push-down automata), a visibly push-down automaton of specific
structure and semantics.
Unweighted shortest path search in graphs.
A concept for supporting destructive modifications, e.g., removal of states.
A graph that supports (desirably efficient) removal of nodes and edges.
A simple automaton, i.e., a
SimpleTS with a finite number of states.Abstractions for
SimpleDeterministicAutomatons.Interface for an
integer abstraction that abstracts both states and input symbols to
integers.SimpleDeterministicAbstractions.FullIntAbstractionImpl<I,A extends SimpleDeterministicAbstractions.StateIntAbstraction<I>>
Base class implementing the default way of obtaining a
SimpleDeterministicAbstractions.FullIntAbstractionImpl, i.e., building on top of a
SimpleDeterministicAbstractions.StateIntAbstractionImpl and a mapping from integers to (concrete) input symbols.Basic interface for integer abstractions of automata.
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().Interface for
integer abstractions of an automaton that operate on non-abstracted input
symbols (i.e., input symbols are of type I).SimpleDeterministicAbstractions.StateIntAbstractionImpl<S,I,A extends SimpleDeterministicAutomaton<S,I>>
Base class implementing the default way of obtaining a
SimpleDeterministicAbstractions.StateIntAbstraction.A simple deterministic automaton.
A simple deterministic transition system.
An edge in an
AbstractCompactGraph.The finite version of a
IndefiniteSimpleGraph.Basic interface for integer abstractions of graphs.
A very simple graph realization, where nodes can be arbitrary Java objects.
A simple transition system.
A specialized implementation for
Alphabets containing only a single symbol.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.An extension of
SizeDFAModelCheckerCache that additionally implements ModelCheckerLassoCache.DFAModelCheckerLassoCache.Mealy version of
SizeDFAModelCheckerCache.Mealy version of
SizeDFAModelCheckerLassoCache.An extended collection interface.
A double-ended queue (deque), allowing access, removal and insertion of elements both at the beginning and the end.
A priority queue interface.
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.Priority queue interface.
Sequence interface.
A class used to store
ProceduralModalProcessGraph-specific data for the SolverHistory.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.Stores internal information produced during the update of a node in
AbstractDDSolver.A system of procedural automata.
Operations on
SPAs.A system of procedural Mealy machines.
Operations on
SPMMs.A conformance test iterator for
SPMMs that is based on the W-method.Result interface for the single-source shortest path (SSSP) problem.
A simplified stack implementation that allows to store integer values.
A stack-based implementation for the (instrumented) language of an
SBA.A stack-based implementation for the (instrumented) language of an
SPA.A stack-based implementation for the (instrumented) transductions of an
SPMM.A stack-based state in a procedural system.
A state configuration of an MMLT.
Utility class to combine an entity (e.g. a location) with stack information.
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.
An interface for translating between automaton states and their primitive representations as integers.
Concept for transition systems, that can for each state return the set of input symbols for which successor states
are defined.
State output concept.
A state output automaton is a
deterministic suffix output automaton that
produces outputs based on its state outputs.Utility class for constructing state signatures used for classifying states during minimization / bisimulation,.
An
ADD solver for generic, string-based formulas.A
BDD solver for generic, string-based formulas.Class for transforming integer index values into string values (using Latin characters, therefore effectively
realizing a radix-26 representation of numbers).
Combines multiple string outputs by concatenating them and using
| as separator.A default implementation that maps abstract input symbol to their
String representations while adding an
incrementing number to mapped call symbols.Miscellaneous utility functions for
Strings.A strong reference wrapper, complying to the
Ref interface.A subsequential transducer (or SST) is an
DeterministicOutputTS whose state and transition properties are
output-words.Utility methods of
SubsequentialTransducers.Feature for transition systems 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.
Interface for declaring that a data structure supports adding new alphabet symbols after its instantiation.
A symbol combiner deterministically maps between multiple output symbols and a single representative.
Markup-interface for symbolic timed inputs.
A generator for random
NFAs as described in the paper
Experimental Evaluation of Classical Automata Constructions
by Deian Tabakov and Moshe Y Vardi.Facade for TAF (textual automaton format) parsing.
Facade for TAF (textual automaton format) writing.
Depth-first traversal visitor realizing Tarjan's algorithm for finding all strongly-connected components (SCCs) in a
graph, as described in Depth-First Search and Linear Graph Algorithms.
Markup-interface for concrete, time-sensitive inputs.
Output that may occur with some or no delay.
Stores information about timers that expire after a given time from now.
An input that causes a delay until the next timeout.
Provides information about a timer that is stored in an MMLT.
The timeout symbol of a timer.
An input that represents multiple subsequent time steps.
Utility interface for serializing
AbstractPropertyTransformer implementations.Transition output concept.
A transition output automaton is a
deterministic suffix output automaton
that produces outputs based on its transition outputs.Transition system interface.
Immutable triple class.
Java representation of a "true" (sub-)formula.
TSComposition<S1,S2,I,T1,T2,TS1 extends TransitionSystem<S1,I,T1>,TS2 extends TransitionSystem<S2,I,T2>>
The type of
TSTraversalAction to be performed.Visitor interface for transition system traversals.
An
ADD solver for strongly-typed formulas.A
BDD solver for strongly-typed formulas.A delegating input stream that throws an exception when closed.
A delegating output stream that throws an exception when closed.
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.
An undirected graph.
The well-known disjoint-set forest data structure for dealing with partitions on a fixed-range integer domain.
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.
A universal automaton is a generalized representation of automata, with unified access to the properties of states
and transitions.
Convenience interface that describes an automaton with finite syntactic and finite semantic state space.
A default implementation for
AbstractCompactDeterministic that uses CompactTransition as transition
type and supports various types of state and transition properties.A refinement of
UniversalCompactDet that additionally implements
MutableDeterministic.RegularAutomaton so that structural determinism and finiteness coincides with semantic
determinism and finiteness.A
AbstractCompactSimpleDeterministic-based implementation for automata that need to store generic state
properties.Abstractions for
UniversalDeterministicAutomatons.Interface for
full integer abstractions of a
UniversalDeterministicAutomaton.UniversalDeterministicAbstractions.FullIntAbstractionImpl<I,T,SP,TP,A extends UniversalDeterministicAbstractions.StateIntAbstraction<I,T,SP,TP>>
Base interface for
integer abstractions of a
UniversalDeterministicAutomaton.Interface for
state integer abstractions of a
UniversalDeterministicAutomaton.UniversalDeterministicAbstractions.StateIntAbstractionImpl<S,I,T,SP,TP,A extends UniversalDeterministicAutomaton<S,I,T,SP,TP>>
A
DeterministicAutomaton with state and transition properties.Convenience interface that describes an automaton with finite syntactic and finite semantic state space.
Universal deterministic transition system.
Interface for
node integer abstractions of a UniversalGraph.A universal graph, i.e., with (possibly empty) node and edge properties.
A "universal" transition system, which captures the possibility to assign properties to states and transitions.
This class implements a collection for storing objects in no particular order.
Valmari's algorithm for computing the relational coarsest partition as presented in Simple Bisimilarity Minimization in O(m log n) Time by Antti
Valmari.
A refinable partition data structure.
Utility methods for extracting various automaton types from
Valmari objects.Utility methods for initializing
Valmari objects from various automaton types.Java representation of an "X" (sub-)formula.
Enum to use for indicating if a node/state has been visited.
A utility class for rendering
IncrementalMealyBuilders.Helper interface for providing additional styling properties for plotting graphs.
Alphabet definition for visible push-down automata.
Classifies an input symbol either as a call symbol, an internal symbol, or a return symbol.
Utility class used to wrap input symbols of a
VPAlphabet.A weak reference wrapper, complying to the
Ref interface.This class implements a
Supplier that randomly delegates to one of several (sub-)suppliers.A tree-like
Graph that represents the BFS-style exploration of the tableau generated by the
WitnessTreeExtractor.A utility class that represents a current configuration (node property) in the
WitnessTree.Iterator that returns test words generated by the W method.
A word is an ordered sequence of symbols.
A class for dynamically building
Words.Iterator that returns test words generated by the partial W method.