# All Classes

- All Classes Interface Summary Class Summary Enum Summary Exception Summary Annotation Types Summary
  Class | Description
  --- | ---
  AbstractCachedStatesAutomaton<S,​A extends OmegaAcceptance> |
  AbstractImplicitAutomaton<S,​A extends OmegaAcceptance> |
  AcceptanceOptimizations |
  AcceptanceOptimizations.AcceptanceOptimizationTransformer |
  Aig |
  AigConsumer |
  AigerPrinter |
  AigFactory |
  AigPrintable |
  AllAcceptance |
  AnnotatedLDBA<S,​T extends LtlLanguageExpressible,​B extends GeneralizedBuchiAcceptance,​X,​Y> |
  AnnotatedState<S> |
  AnnotatedStateOptimisation |
  AsymmetricEvaluatedFixpoints |
  AsymmetricEvaluatedFixpoints.DeterministicAutomata |
  AsymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance> |
  AsymmetricProductState |
  Automaton<S,​A extends OmegaAcceptance> | The base interface providing read access to an automaton.
  Automaton.EdgeMapVisitor<S> |
  Automaton.EdgeTreeVisitor<S> |
  Automaton.EdgeVisitor<S> |
  Automaton.PreferredEdgeAccess |
  Automaton.Property |
  Automaton.Visitor<S> |
  AutomatonFactory |
  AutomatonOperations |
  AutomatonReader |
  AutomatonReader.HoaState |
  AutomatonUtil |
  Biconditional | Biconditional.
  BinaryModalOperator |
  BinaryVisitor<P,​R> |
  BlockingModalOperatorsVisitor |
  BooleanConstant |
  BooleanExpressions |
  BreakpointState<E> |
  BreakpointState<S> |
  BuchiAcceptance |
  BuchiDegeneralization |
  CEntryPoint |
  CoBuchiAcceptance |
  Collections3 |
  Conjunction |
  Converter |
  DaemonThreadFactory |
  DecomposedDPA |
  DecomposedDPA.Reference |
  DeduplicationRewriter |
  DefaultCli |
  DelagBuilder |
  DeterministicAutomaton<S,​T> |
  DeterministicConstructions |
  DeterministicConstructions.CoSafety |
  DeterministicConstructions.FgSafety |
  DeterministicConstructions.GCoSafety |
  DeterministicConstructions.GfCoSafety |
  DeterministicConstructions.Safety |
  DeterministicConstructions.Tracking |
  Disjunction |
  DPA2Safety<S> |
  Edge<S> | This class (with specialised subclasses) represents edges of automata including their acceptance membership.
  EdgeMapAutomatonMixin<S,​A extends OmegaAcceptance> | Mixin interface for implementing an automaton by `Automaton.edgeMap(Object)`.
  Edges |
  EdgesAutomatonMixin<S,​A extends OmegaAcceptance> | Mixin interface for implementing an automaton by `Automaton.edges(Object, BitSet)`.
  EdgeTreeAutomatonMixin<S,​A extends OmegaAcceptance> | Mixin interface for implementing an automaton by `Automaton.edgeTree(Object)`.
  Either<A,​B> |
  EmersonLeiAcceptance |
  Environment | The environment makes global configuration available to all parts of the pipeline.
  EquivalenceClass | EquivalenceClass interface.
  EquivalenceClassFactory |
  EverythingIsNonnullByDefault |
  ExternalTranslator |
  Factories |
  FactorySupplier |
  FGX2DPA |
  Fixpoints |
  FOperator | Finally.
  Formula |
  Formula.LogicalOperator |
  Formula.ModalOperator |
  Formula.TemporalOperator |
  FormulaIsomorphism |
  Formulas |
  FrequencyG |
  FrequencyG.Comparison |
  FrequencyG.Limes |
  Game<S,​A extends OmegaAcceptance> |
  Game.Owner |
  GameFactory |
  GameUtil |
  GameViews |
  GameViews.Node<S> | A state of the split game.
  GeneralizedBuchiAcceptance |
  GeneralizedRabinAcceptance | Generalized Rabin Acceptance - OR (Fin(i) and AND Inf(j)).
  GeneralizedRabinAcceptance.Builder |
  GeneralizedRabinAcceptance.RabinPair |
  GeneralizedRabinAcceptanceOptimizations |
  GenericConstructions |
  GOperator | Globally.
  GuardedStream | Wrappers for streams which only forward a `OutputStream.flush()` upon `OutputStream.close()`.
  HashedTuple |
  HoaPrinter |
  HoaPrinter.HoaOption |
  IARBuilder<R> |
  IARState<R> |
  ImplicitNonDeterministicEdgeTreeAutomaton<S,​A extends OmegaAcceptance> |
  InputReader | Input readers are tasked with providing input to the processing pipeline.
  InputReaders |
  InputReaders.CheckedCallback |
  IntBiConsumer |
  IntVisitor |
  JBddSupplier |
  LabelledAig |
  LabelledFormula |
  LabelledSplit |
  LabelledTree<L1,​L2> |
  LabelledTree.Leaf<L1,​L2> |
  LabelledTree.Node<L1,​L2> |
  LanguageAnalysis |
  LanguageContainment |
  LanguageEmptiness |
  LanguageMembership |
  LatexPrintVisitor |
  LegacyFactory | Deprecated.
  Literal |
  LiteralMapper |
  LiteralMapper.ShiftedFormula |
  LTL2DAFunction |
  LTL2DAFunction.Constructions |
  LTL2DAModule |
  LTL2DGRAModule |
  LTL2DPAFunction |
  LTL2DPAFunction.Configuration |
  LTL2DPAModule |
  LTL2DRAModule |
  LTL2LDBAModule |
  LTL2LDGBAModule |
  LTL2NAFunction |
  LTL2NAFunction.Constructions |
  LTL2NAModule |
  LTL2NBAModule |
  LTL2NGBAModule |
  LtlLanguageExpressible |
  LTLLexer |
  LtlParser |
  LTLParser |
  LTLParser.AndExpressionContext |
  LTLParser.AtomExpressionContext |
  LTLParser.BinaryExpressionContext |
  LTLParser.BinaryOpContext |
  LTLParser.BinaryOperationContext |
  LTLParser.BinaryUnaryContext |
  LTLParser.BoolContext |
  LTLParser.BooleanContext |
  LTLParser.ComparisonContext |
  LTLParser.DoubleQuotedVariableContext |
  LTLParser.ExpressionContext |
  LTLParser.FormulaContext |
  LTLParser.FractionContext |
  LTLParser.FrequencyOpContext |
  LTLParser.FrequencySpecContext |
  LTLParser.NestedContext |
  LTLParser.OrExpressionContext |
  LTLParser.ProbabilityContext |
  LTLParser.SingleQuotedVariableContext |
  LTLParser.UnaryAtomContext |
  LTLParser.UnaryExpressionContext |
  LTLParser.UnaryOpContext |
  LTLParser.UnaryOperationContext |
  LTLParser.VariableContext |
  LTLParserBaseListener | This class provides an empty implementation of `LTLParserListener`, which can be extended to create a listener which only needs to handle a subset of the available methods.
  LTLParserBaseVisitor<T> | This class provides an empty implementation of `LTLParserVisitor`, which can be extended to create a visitor which only needs to handle a subset of the available methods.
  LTLParserListener | This interface defines a complete listener for a parse tree produced by `LTLParser`.
  LTLParserVisitor<T> | This interface defines a complete generic visitor for a parse tree produced by `LTLParser`.
  Monitor<F extends UnaryModalOperator> |
  MOperator | Strong Release.
  MutableAutomaton<S,​A extends OmegaAcceptance> | A mutation interface extending `Automaton`.
  MutableAutomatonFactory |
  MutableAutomatonUtil |
  MutableAutomatonUtil.Sink |
  NBA2DPA |
  NBA2LDBA |
  NBA2LDBA.LDBA<S> |
  NonDeterministicConstructions |
  NonDeterministicConstructions.CoSafety |
  NonDeterministicConstructions.FgSafety |
  NonDeterministicConstructions.GfCoSafety |
  NonDeterministicConstructions.Safety |
  NonDeterministicConstructions.Tracking |
  NoneAcceptance |
  NormalForms |
  OmegaAcceptance |
  OmegaAcceptanceOptimizations |
  OutputWriter | The final piece of every pipeline, formatting the produced results and writing them on some output.
  OutputWriter.Binding |
  OutputWriters |
  OutputWriters.AutomatonStats |
  OutputWriters.ToHoa | Converts any `HOA printable` object to its corresponding HOA representation.
  OwlModule |
  OwlModuleParser<M extends OwlModule> |
  OwlModuleParser.ReaderParser |
  OwlModuleParser.TransformerParser |
  OwlModuleParser.WriterParser |
  OwlModuleRegistry | A registry holding all modules used to parse the command line.
  OwlModuleRegistry.OwlModuleNotFoundException |
  OwlModuleRegistry.Type |
  OwlParser |
  ParityAcceptance |
  ParityAcceptance.Parity |
  ParityAcceptanceOptimizations |
  ParityGameSolver |
  ParityUtil |
  PartialConfigurationParser | Utility class used to parse a simplified command line (single exposed module with rest of the pipeline preconfigured).
  PartialModuleConfiguration |
  PartialModuleConfiguration.Constructor |
  Pipeline |
  PipelineException |
  PipelineExecutionContext | Holds information about an execution originating from a particular input.
  PipelineParser | Utility class used to parse a `pipeline` description based on a `registry`.
  PipelineParser.ModuleParseException |
  PipelineRunner | Helper class to execute a specific pipeline with created input and output streams.
  Predicates |
  PrintVisitor |
  ProductState |
  PromisedSet |
  PropositionalFormula |
  PropositionalIntVisitor | Visitor skeleton implementation that views the formula as propositional formula.
  PropositionalVisitor<T> | Visitor skeleton implementation that views the formula as propositional formula.
  PullUpXVisitor |
  PullUpXVisitor.XFormula |
  RabinAcceptance | This class represents a Rabin acceptance.
  RabinAcceptance.Builder |
  RabinDegeneralization |
  RabinizerBuilder | Central class handling the Rabinizer construction.
  RabinizerConfiguration |
  RabinizerState |
  RankingState<S> |
  Rewriter |
  Rewriter.ToCoSafety |
  Rewriter.ToSafety |
  RobustLtlInputReader |
  RobustLtlParser |
  Robustness |
  ROperator | Weak Release.
  RoundRobinState<E> |
  RunUtil |
  SafetyAutomaton |
  SafetyCoreDetector |
  SccDecomposition<S> | Finds the SCCs of a given graph / transition system using Tarjan's algorithm.
  Selector |
  ServerCli |
  ServerRunner |
  SimplifierFactory |
  SimplifierFactory.Mode |
  SimplifierTransformer |
  Split |
  State<T> |
  StringUtil |
  SuccessorFunction<S> |
  SymmetricDRAConstruction<R extends GeneralizedRabinAcceptance> |
  SymmetricEvaluatedFixpoints |
  SymmetricEvaluatedFixpoints.DeterministicAutomata |
  SymmetricEvaluatedFixpoints.NonDeterministicAutomata |
  SymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance> |
  SymmetricNBAConstruction<B extends GeneralizedBuchiAcceptance> |
  SymmetricProductState |
  SyntacticFragment |
  SyntacticFragments |
  Synthesis |
  TokenErrorListener |
  Transformer | Transformers are the central pieces of the pipeline concept.
  Transformer.Instance |
  Transformers |
  Transformers.SimpleTransformer |
  Tuple |
  TwoPartAutomaton<A,​B,​C extends OmegaAcceptance> |
  TypeUtil |
  UltimatelyPeriodicWord |
  UnabbreviateVisitor |
  UnaryModalOperator |
  UOperator | Strong Until.
  UpwardClosedSet | Bucket-based implementation of an upward-closed set.
  ValuationSet |
  ValuationSetFactory |
  ValuationTree<E> |
  ValuationTree.Leaf<E> |
  ValuationTree.Node<E> |
  ValuationTrees |
  Views |
  Views.AutomatonView<S,​A extends OmegaAcceptance> |
  Visitor<R> |
  WOperator | Weak Until.
  XDepthVisitor |
  XOperator | Next.