All Classes Interface Summary Class Summary Enum Summary Exception Summary Annotation Types Summary
| Class |
Description |
| AbstractImmutableAutomaton<S,A extends OmegaAcceptance> |
This abstract class implements storage and retrieval of commonly fixed values, and overrides the
default implementations for Automaton.states(), Automaton.accept(Visitor) in
order to cache the set of reachable states for later use.
|
| AbstractImmutableAutomaton.NonDeterministicEdgeMapAutomaton<S,A extends OmegaAcceptance> |
This class provides a skeleton implementation to create a non-deterministic on-the-fly
constructed automaton that uses ValuationSet as the main
representation of the transition relation.
|
| AbstractImmutableAutomaton.NonDeterministicEdgesAutomaton<S,A extends OmegaAcceptance> |
This class provides a skeleton implementation to create a non-deterministic on-the-fly
constructed automaton.
|
| AbstractImmutableAutomaton.NonDeterministicEdgeTreeAutomaton<S,A extends OmegaAcceptance> |
This class provides a skeleton implementation to create a non-deterministic on-the-fly
constructed automaton that uses ValuationTree as the main
representation of the transition relation.
|
| AbstractImmutableAutomaton.SemiDeterministicEdgesAutomaton<S,A extends OmegaAcceptance> |
This class provides a skeleton implementation to create a semi-deterministic on-the-fly
constructed automaton.
|
| AcceptanceOptimizations |
|
| AcceptanceOptimizations.AcceptanceOptimizationTransformer |
|
| Aig |
|
| AigConsumer |
|
| AigerPrinter |
|
| AigFactory |
|
| AigPrintable |
|
| AllAcceptance |
|
| AnnotatedLDBA<S,T extends LtlLanguageExpressible,B extends GeneralizedBuchiAcceptance,X,Y> |
Translation-specific internal representation of LDBAs.
|
| AnnotatedState<S> |
|
| AnnotatedStateOptimisation |
|
| ArraysSupport |
|
| AsymmetricEvaluatedFixpoints |
|
| AsymmetricEvaluatedFixpoints.DeterministicAutomata |
|
| AsymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance> |
|
| AsymmetricProductState |
|
| AsymmetricRankingState |
|
| 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> |
|
| AutomatonUtil |
|
| AutomatonUtil.LimitDeterministicGeneralizedBuchiAutomaton<S,B extends GeneralizedBuchiAcceptance> |
|
| BackwardDirectSimulation<S> |
|
| Biconditional |
Biconditional.
|
| BinaryVisitor<P,R> |
|
| BitSetUtil |
Utility functions to convert from and to bitsets.
|
| BlockingElements |
|
| BooleanConstant |
|
| BooleanExpressions |
|
| BooleanOperations |
This class provides standard boolean operations (union, intersection) on automata.
|
| BreakpointState<S> |
|
| BuchiAcceptance |
|
| BuchiDegeneralization |
This class provides a conversion from generalised Büchi automata into Büchi automata.
|
| BuchiDegeneralization.IndexedState<S> |
|
| BuchiSimulation |
|
| BuchiSimulationArguments |
|
| CAutomaton |
|
| CAutomaton.Acceptance |
|
| CDecomposedDPA |
|
| CDecomposedDPA.RealizabilityStatus |
|
| CDecomposedDPA.Structure |
|
| CDecomposedDPA.Structure.NodeType |
|
| CDoubleArrayList |
|
| CIntArrayList |
|
| CInterface |
|
| CLabelledFormula |
|
| CLabelledFormula.AtomicPropositionStatus |
|
| CoBuchiAcceptance |
|
| Collections3 |
|
| ColorRefinement<S> |
Computes direct simulation relation of an automaton based on the color refinement algorithm.
|
| ColorRefinement.Neighborhood |
Represents the neighborhood of a state.
|
| ColorRefinement.NeighborType |
Represents a neighbor type consisting of color and associated valuation.
|
| CombinationGenerator |
|
| CombineUntilVisitor |
|
| Conjunction |
|
| Converter |
|
| DecomposedDPA |
|
| DeduplicationRewriter |
|
| DefaultCli |
|
| DelagBuilder |
|
| DeterministicConstructions |
|
| DeterministicConstructions.BreakpointStateAccepting |
|
| DeterministicConstructions.BreakpointStateRejecting |
|
| DeterministicConstructions.CoSafety |
|
| DeterministicConstructions.CoSafetySafety |
|
| DeterministicConstructions.GfCoSafety |
|
| DeterministicConstructions.Safety |
|
| DeterministicConstructions.SafetyCoSafety |
|
| DeterministicConstructions.Tracking |
|
| DeterministicConstructionsPortfolio<A extends OmegaAcceptance> |
|
| Determinization |
|
| Determinization.BreakpointState<S> |
|
| Disjunction |
|
| DPA2Safety<S> |
|
| Edge<S> |
This class (with specialised subclasses) represents edges of automata including their acceptance
membership.
|
| EdgeMapAutomatonMixin<S,A extends OmegaAcceptance> |
|
| Edges |
|
| EdgesAutomatonMixin<S,A extends OmegaAcceptance> |
|
| EdgeTreeAutomatonMixin<S,A extends OmegaAcceptance> |
|
| Either<A,B> |
|
| Either.Type |
|
| EmersonLeiAcceptance |
|
| EmptyAutomaton<S,A extends OmegaAcceptance> |
|
| EmulatedCDoublePointer |
|
| EmulatedCIntPointer |
|
| Environment |
The environment makes global configuration available to all parts of the pipeline.
|
| EquivalenceClass |
A propositional equivalence class of an LTL formula.
|
| EquivalenceClassFactory |
A factory for creating propositional equivalence classes for LTL formulas.
|
| EverythingIsNonnullByDefault |
|
| ExternalTranslator |
|
| ExternalTranslator.InputMode |
|
| Factories |
|
| FactorySupplier |
|
| Fixpoints |
|
| FOperator |
Finally.
|
| Formula |
|
| Formula.BinaryTemporalOperator |
|
| Formula.NaryPropositionalOperator |
|
| Formula.PropositionalOperator |
|
| Formula.TemporalOperator |
|
| Formula.UnaryTemporalOperator |
|
| FormulaIsomorphism |
|
| Formulas |
|
| ForwardDelayedSimulation<S> |
|
| ForwardDirectLookaheadSimulation<S> |
|
| ForwardDirectSimulation<S> |
Simulation type for forward-direct multipebble simulation games.
|
| ForwardFairSimulation<S> |
|
| Game<S,A extends OmegaAcceptance> |
|
| Game.Owner |
|
| GameFactory |
|
| GameUtil |
|
| GameViews |
|
| GameViews.Node<S> |
A state of the split game.
|
| GeneralizedBuchiAcceptance |
|
| GeneralizedCoBuchiAcceptance |
|
| GeneralizedRabinAcceptance |
Generalized Rabin Acceptance - OR (Fin(i) and AND Inf(j)).
|
| GeneralizedRabinAcceptance.Builder |
|
| GeneralizedRabinAcceptance.RabinPair |
|
| GeneralizedRabinAcceptanceOptimizations |
|
| GenericConstructions |
|
| GfgCoBuchiMinimization |
This class implements [ICALP'19] minimization of GFG automata.
|
| GOperator |
Globally.
|
| GuardedStream |
|
| HashMapAutomaton<S,A extends OmegaAcceptance> |
|
| HoaReader |
|
| HoaReader.HoaState |
|
| HoaWriter |
|
| HoaWriter.HoaOption |
|
| IARBuilder<R> |
|
| IARState<R> |
|
| InputReaders |
|
| IntVisitor |
|
| JBddSupplier |
|
| LabelledAig |
|
| LabelledFormula |
|
| LabelledSplit |
|
| LanguageAnalysis |
|
| LanguageContainment |
|
| LanguageEmptiness |
|
| LanguageMembership |
|
| LatexPrintVisitor |
|
| LegacyFactory |
Deprecated. |
| Literal |
|
| LiteralMapper |
|
| LiteralMapper.ShiftedLabelledFormula |
|
| LTL2DAFunction |
|
| LTL2DAModule |
|
| LTL2DGRAModule |
|
| LTL2DPAFunction |
|
| LTL2DPAFunction.Configuration |
|
| LTL2DPAModule |
|
| LTL2DRAModule |
|
| LTL2LDBAModule |
|
| LTL2LDGBAModule |
|
| LTL2NAFunction |
|
| LTL2NAModule |
|
| LTL2NBAModule |
|
| LTL2NGBAModule |
|
| LTL2NormalFormModule |
|
| LtlfParser |
|
| LtlfToLtlTranslator |
|
| LtlfToLtlTranslator.LtlfToLtlVisitor |
|
| LtlfToLtlTranslator.LtlfToLtlVisitor.PushNegOneDownVisitor |
|
| LtlLanguageExpressible |
|
| LTLLexer |
|
| LtlParser |
|
| LTLParser |
|
| LTLParser.AndExpressionContext |
|
| LTLParser.AtomExpressionContext |
|
| LTLParser.BinaryExpressionContext |
|
| LTLParser.BinaryOpContext |
|
| LTLParser.BinaryOperationContext |
|
| LTLParser.BinaryUnaryContext |
|
| LTLParser.BoolContext |
|
| LTLParser.BooleanContext |
|
| LTLParser.DoubleQuotedVariableContext |
|
| LTLParser.ExpressionContext |
|
| LTLParser.FormulaContext |
|
| LTLParser.NestedContext |
|
| LTLParser.OrExpressionContext |
|
| 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.
|
| MonitorState |
|
| MOperator |
Strong Release.
|
| MultiPebble<S> |
Abstracts multiple pebbles controlled by Duplicator in a multipebble simulation game.
|
| MutableAutomaton<S,A extends OmegaAcceptance> |
|
| MutableAutomatonUtil |
|
| MutableAutomatonUtil.Sink |
|
| NBA2DPA |
|
| NBA2LDBA |
|
| NbaAdjMat<S> |
|
| NbaDet |
This class provides a conversion from non-deterministic Büchi automata
into deterministic parity automata.
|
| NbaDetArgs |
|
| NbaDetArgs.Builder |
|
| NbaDetConf<S> |
This is the structure containing all required information that is used in the
determinization process and is obtained based on an NbaDetArgs instance.
|
| NbaDetConf.UpdateMode |
|
| NbaDetConfSets |
these sets reflect the different determinisation components to be used in the DetState
i.e.
|
| NbaDetState<S> |
This is the state type of the deterministic parity automaton produced by nbadet.
|
| NbaLangInclusions |
This class glues available algorithms that can underapprox.
|
| NbaLangInclusions.SimType |
Register new simulation algorithms here.
|
| NbaSccInfo<S> |
This class wraps SccDecomposition, assigns each SCC an integer ID (in topological order)
and provides additional lookup tables to check various SCC properties and the SCC ID of states.
|
| NbaSimAlgorithm<S,T> |
Interface that all pluggable language inclusion / simulation algorithms should implement.
|
| Negation |
|
| NonDeterministicConstructions |
|
| NonDeterministicConstructions.CoSafety |
|
| NonDeterministicConstructions.FgSafety |
|
| NonDeterministicConstructions.GfCoSafety |
|
| NonDeterministicConstructions.Safety |
|
| NonDeterministicConstructions.Tracking |
|
| NonDeterministicConstructionsPortfolio<A extends OmegaAcceptance> |
|
| NormalForms |
|
| Normalisation |
|
| NullablePair<A,B> |
|
| OinkGameSolver |
|
| OinkGameSolver.OinkExecutionException |
Abstracts potential errors when executing oink to solve a game.
|
| OmegaAcceptance |
|
| OmegaAcceptanceCast |
This class provides functionality to cast an automaton to an automaton with a more generic
acceptance condition.
|
| OutputWriters |
|
| OutputWriters.AutomatonStats |
|
| OutputWriters.ToHoa |
|
| OwlModule<M extends OwlModule.Instance> |
|
| OwlModule.AutomatonTransformer |
Derived transformer that casts the argument to an Automaton and optionally converts
the acceptance condition if possible.
|
| OwlModule.Constructor<M> |
|
| OwlModule.InputReader |
Input readers are tasked with providing input to the processing pipeline.
|
| OwlModule.Instance |
|
| OwlModule.LabelledFormulaTransformer |
|
| OwlModule.OutputWriter |
The final piece of every pipeline, formatting the produced results and writing them on some
output.
|
| OwlModule.Transformer |
Transformers are the central pieces of the pipeline concept.
|
| OwlModuleRegistry |
A registry holding all modules used to parse the command line.
|
| OwlModuleRegistry.OwlModuleNotFoundException |
|
| OwlModuleRegistry.Type |
|
| OwlParser |
|
| OwlVersion |
|
| OwlVersion.NameAndVersion |
|
| Pair<A,B> |
|
| ParityAcceptance |
|
| ParityAcceptance.Parity |
|
| ParityAcceptanceOptimizations |
|
| ParityGameSolver |
|
| ParityGameSolver.WinningRegions<S> |
|
| ParityUtil |
|
| PartialConfigurationParser |
Utility class used to parse a simplified command line (single exposed module with rest of the
pipeline preconfigured).
|
| PartialModuleConfiguration |
|
| Pebble<S> |
Abstraction of a single pebble in a multipebble simulation game.
|
| Pipeline |
|
| PipelineException |
|
| PipelineParser |
|
| PipelineParser.ModuleParseException |
|
| Predicates |
|
| PreprocessorVisitor |
|
| PrintVisitor |
|
| ProductState<T> |
|
| ProductState |
|
| 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 |
|
| RabinDegeneralization.DegeneralizedRabinState<S> |
|
| RabinizerBuilder |
Central class handling the Rabinizer construction.
|
| RabinizerConfiguration |
|
| RabinizerState |
|
| RankedSlice |
type/wrapper of ranked slices, which are just tuples of disjoint sets, with entries that are
additionally to the index order also ranked by some extra total order (i.e.
|
| RankingState<S> |
|
| Rewriter |
|
| Rewriter.ToCoSafety |
|
| Rewriter.ToSafety |
|
| RobustLtlInputReader |
|
| RobustLtlParser |
|
| Robustness |
|
| ROperator |
Weak Release.
|
| RoundRobinState<E> |
|
| RunUtil |
|
| SccDecomposition<S> |
This class provides a decomposition into strongly connected components (SCCs) of a directed graph
given by either an Automaton or a SuccessorFunction.
|
| Selector |
|
| ServerCli |
|
| SimplifierFactory |
|
| SimplifierFactory.Mode |
|
| SimplifierTransformer |
|
| SimulationGame<S,T extends SimulationType.SimulationState<S>> |
Wrapper class that takes a simulationType and constructs the actual game itself based on the
state and transition function defined within the concrete simulationType.
|
| SimulationStates |
|
| SimulationStates.LookaheadSimulationState<S> |
|
| SimulationStates.MultipebbleSimulationState<S> |
Holds all information necessary to implement forward multipebble simulations.
|
| SimulationType<S,T extends SimulationType.SimulationState<S>> |
|
| SimulationType.SimulationState<S> |
|
| SimulationUtil |
|
| SingletonAutomaton<S,A extends OmegaAcceptance> |
|
| SmartSucc<S> |
This class acts like a "smart cache" for the states produced during NBA determinization.
|
| Split |
|
| SplitUntilVisitor |
|
| State<T> |
|
| Statistics |
|
| StringUtil |
|
| SuccessorFunction<S> |
|
| SymmetricDRAConstruction<R extends GeneralizedRabinAcceptance> |
|
| SymmetricEvaluatedFixpoints |
|
| SymmetricEvaluatedFixpoints.DeterministicAutomata |
|
| SymmetricEvaluatedFixpoints.NonDeterministicAutomata |
|
| SymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance> |
|
| SymmetricNBAConstruction<B extends GeneralizedBuchiAcceptance> |
|
| SymmetricProductState |
|
| SymmetricRankingState |
|
| SymmetricRankingState |
|
| SyntacticFragment |
|
| SyntacticFragments |
|
| SyntacticFragments.FormulaClass |
|
| SyntacticFragments.Type |
|
| SyntacticSimplifier |
|
| Synthesis |
|
| TokenErrorListener |
|
| ToStateAcceptanceFixed |
Convert automaton to state-based acceptance.
|
| Transition<S> |
|
| TrieMap<K,V> |
A TrieMap is a Map with sequences as keys that are organized in a Trie for value retrieval.
|
| TriFunction<A,B,C,R> |
|
| TwoPartAutomaton<A,B,C extends OmegaAcceptance> |
|
| UltimatelyPeriodicWord |
|
| UnabbreviateVisitor |
|
| 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.Filter<S> |
|
| Views.Filter.Builder<S> |
|
| Visitor<R> |
|
| WOperator |
Weak Until.
|
| XDepthVisitor |
|
| XOperator |
Next.
|
| ZielonkaGameSolver |
|