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> |
|
| Edges |
|
| EdgesAutomatonMixin<S,A extends OmegaAcceptance> |
|
| EdgeTreeAutomatonMixin<S,A extends OmegaAcceptance> |
|
| 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 |
|
| 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> |
|
| 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 |
|
| 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 |
|
| 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.
|