All Classes Class Summary Enum Summary
| Class |
Description |
| ABC |
|
| AnalysisAgainstSpectra |
|
| AutomataBasedModelCounting |
|
| AutomataBasedModelCountingSpecificationFitness |
The multi-objective fitness function of AuRUS — the compass that guides the
genetic search — with the semantic component estimated via approximate
bounded model counting over automaton transfer matrices.
|
| Buchi2Graph |
|
| Count |
|
| CountMain |
|
| CountREModels |
|
| CountRltlConv |
|
| EmersonLeiAutomatonBasedModelCounting<S> |
AuRUS's approximate bounded LTL model counter (the ApMC of the
paper): estimates the number of satisfying traces of bounded length of an
LTL formula by a single linear-algebra computation over the formula's
automaton.
|
| Formula2Automaton<S> |
|
| FormulaMutator |
|
| FormulaStrengthening |
The strengthening mutation mode of AuRUS: rewrites an LTL formula
(in negation normal form) into a semantically stronger one, i.e.
|
| FormulaToRE |
|
| FormulaUtils |
|
| FormulaWeakening |
The weakening mutation mode of AuRUS: rewrites an LTL formula (in
negation normal form) into a semantically weaker one, i.e.
|
| GeneralFormulaMutator |
|
| GenuineSolutionsAnalysis |
|
| LTLSolver |
|
| LTLSolver.SolverResult |
|
| Main |
Command-line entry point of AuRUS.
|
| MatrixBigIntegerModelCounting |
|
| ModelCountingRanking |
|
| ModelCountingSpecificationFitness |
|
| PotentiallyRealizabilityChecker<S> |
|
| PreciseLTLModelCounter |
|
| PreciseLTLModelCounter.MODEL_COUNTER |
|
| PreciseModelCountingEvaluation |
|
| PreciseModelCountingSpecificationFitness |
|
| PropositionVariablesExtractor |
|
| Rltlconv_LTLModelCounter |
|
| Settings |
Central, static configuration of AuRUS: every knob the genetic search, the
fitness function, the model counter and the external solvers read from.
|
| SolverSyntaxOperatorReplacer |
|
| SolverUtils |
|
| SpecificationChromosome |
The individual of AuRUS's genetic search: a complete assume-guarantee
specification, together with its cached evaluation results.
|
| SpecificationChromosome.SPEC_STATUS |
The evaluation lattice of a candidate specification, ordered from
completely broken to repaired:
|
| SpecificationCrossover |
The crossover operator of AuRUS: recombines two parent
specifications into offspring that mix their assumptions and guarantees,
so that promising fragments discovered in different individuals can meet in
a single candidate.
|
| SpecificationFitness |
|
| SpecificationGeneticAlgorithm |
Main entry point of the AuRUS search: a genetic algorithm that evolves
candidate repairs for an unrealisable assume-guarantee LTL specification.
|
| SpecificationMerger |
|
| SpecificationMutator |
The mutation operator of AuRUS: produces a syntactic variant of a
specification by rewriting one randomly chosen sub-formula of one of its
assumptions or guarantees.
|
| StrixHelper |
Bridge to the external Strix reactive-synthesis tool, used by AuRUS
to check the realisability of a candidate specification — the
status(S') component of the fitness function.
|
| StrixHelper.RealizabilitySolverResult |
Outcome of a Strix realisability query.
|
| StrongSatisfiabilityChecker<S> |
|
| StrongSATSolver<S> |
|
| SubformulaReplacer |
Replaces every occurrence of a given sub-formula with another, throughout
an LTL formula's syntax tree.
|
| SynSemDistanceAnalysis |
|
| TestRunner |
|
| TlsfUtils |
|
| WellSeparationAnalysis |
|