Index (AuRUS API Documentation)

A B C D E F G H I L M N O P R S T U V W
All Classes All Packages

A

ABC - Class in modelcounter
ABC() - Constructor for class modelcounter.ABC
abcDriver - Variable in class modelcounter.ABC
accConditionIsSatisfied(BooleanExpression<AtomAcceptance>, IntArrayList) - Method in class modelcounter.EmersonLeiAutomatonBasedModelCounting: Recursively evaluates the automaton's Emerson-Lei acceptance condition — an arbitrary boolean expression in HOA format over Inf/Fin atoms — against the acceptance sets visited by a single edge.
accConditionIsSatisfied(BooleanExpression<AtomAcceptance>, IntArrayList) - Method in class solvers.PotentiallyRealizabilityChecker
accConditionIsSatisfied(BooleanExpression<AtomAcceptance>, IntArrayList) - Method in class solvers.StrongSatisfiabilityChecker
accConditionIsSatisfied(BooleanExpression<AtomAcceptance>, IntArrayList) - Method in class utils.Formula2Automaton
adaptTLSFSpec(Tlsf) - Static method in class utils.TlsfUtils
allowAssumptionAddition - Static variable in class main.Settings: Allow the genetic operators to introduce brand-new assumptions rather than only modifying existing ones (flags -addA/-addAssumptions, default false).
allowAssumptionRemoval - Static variable in class main.Settings: Allow the genetic operators to drop assumptions entirely (flags -removeA/-removeAssumptions, default false).
allowGuaranteeRemoval - Static variable in class main.Settings: Allow the genetic operators to drop guarantees entirely (flags -removeG/-removeGuarantees, default false).
alphabet - Variable in class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: Atomic propositions of the specification (currently unused; kept for compatibility).
alphabet - Variable in class geneticalgorithm.ModelCountingSpecificationFitness
alphabetSize - Variable in class utils.Formula2Automaton
alphabetSize - Variable in class utils.FormulaToRE
AnalysisAgainstSpectra - Class in main
AnalysisAgainstSpectra() - Constructor for class main.AnalysisAgainstSpectra
apply(Formula) - Method in class owl.ltl.visitors.FormulaMutator
apply(Formula) - Method in class owl.ltl.visitors.FormulaStrengthening: Entry point: applies this visitor to the root of the given formula.
apply(Formula) - Method in class owl.ltl.visitors.FormulaWeakening: Entry point: applies this visitor to the root of the given formula.
apply(Formula) - Method in class owl.ltl.visitors.GeneralFormulaMutator
apply(Formula) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
apply(Formula) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
apply(Formula) - Method in class owl.ltl.visitors.SubformulaReplacer: Entry point: applies the replacement throughout the given formula.
apply(Tlsf, Tlsf, int, int) - Static method in class geneticalgorithm.SpecificationCrossover: Recombines the two parents, applying the given level to each side independently (levels are described in the class documentation; any value other than 0 or 1 selects the sub-formula merge).
applyGeneralMutation(Formula, List<String>) - Static method in class geneticalgorithm.SpecificationMutator: Applies the undirected general mutation to a formula: atoms can be flipped or swapped, unary operators removed, replaced or stacked, and binary connectives exchanged, exploring the syntactic neighbourhood without directional bias.
areAssumptionsSAT() - Method in enum geneticalgorithm.SpecificationChromosome.SPEC_STATUS
areGuaranteesSAT() - Method in enum geneticalgorithm.SpecificationChromosome.SPEC_STATUS
ASSUMPTIONS - geneticalgorithm.SpecificationChromosome.SPEC_STATUS: The assumptions are satisfiable, but the guarantees are not.
automata2RE(Nba) - Method in class modelcounter.Rltlconv_LTLModelCounter
AutomataBasedModelCounting - Class in modelcounter
AutomataBasedModelCounting(Graph<String>, boolean) - Constructor for class modelcounter.AutomataBasedModelCounting
AutomataBasedModelCounting(LabelledFormula, boolean) - Constructor for class modelcounter.AutomataBasedModelCounting
AutomataBasedModelCountingSpecificationFitness - Class in geneticalgorithm: 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.
AutomataBasedModelCountingSpecificationFitness(Tlsf) - Constructor for class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: Creates the fitness function for a given original specification.
automataToRegularExpression(Automaton<S, ? extends OmegaAcceptance>) - Method in class utils.FormulaToRE

B

BASENAME - Variable in class solvers.PreciseLTLModelCounter
bestSolutions - Variable in class geneticalgorithm.SpecificationGeneticAlgorithm: Best candidates collected during the search when realisability is not checked inside the fitness (see Settings.check_REALIZABILITY and Settings.check_STRONG_SAT).
BOTTOM - geneticalgorithm.SpecificationChromosome.SPEC_STATUS: Both the assumptions and the guarantees are unsatisfiable.
BOUND - Variable in class solvers.PreciseLTLModelCounter
Buchi2Graph - Class in modelcounter
Buchi2Graph() - Constructor for class modelcounter.Buchi2Graph
buildFinalStates() - Method in class modelcounter.EmersonLeiAutomatonBasedModelCounting: Builds the indicator column vector v of the accepting states — and this is where the finite-word abstraction (and hence the approximation) lives.
buildInitialStates() - Method in class modelcounter.EmersonLeiAutomatonBasedModelCounting: Builds the indicator row vector u of the initial states: u[0][j] = 1 iff states[j] is an initial state of the automaton, 0 otherwise.
buildInputAutomata(Automaton<S, EmersonLeiAcceptance>, List<String>, List<String>) - Method in class solvers.StrongSATSolver
buildTransferMatrix() - Method in class modelcounter.EmersonLeiAutomatonBasedModelCounting: Builds the weighted transfer matrix T of the automaton: entry T[i][j] is the number of propositional valuations sigma in 2^AP whose edge carries state s_i to state s_j.
buildTransferMatrix(Graph<String>) - Method in class modelcounter.AutomataBasedModelCounting: Build the Transfer Matrix for the given DFA
buildTransferMatrix(Graph<String>) - Method in class modelcounter.MatrixBigIntegerModelCounting: Build the Transfer Matrix for the given DFA

C

CACHET - solvers.PreciseLTLModelCounter.MODEL_COUNTER
calculate(SpecificationChromosome) - Method in class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: Computes the fitness of a candidate repair (the weighted sum described in the class documentation).
calculate(SpecificationChromosome) - Method in class geneticalgorithm.ModelCountingSpecificationFitness
calculate(SpecificationChromosome) - Method in class geneticalgorithm.PreciseModelCountingSpecificationFitness
calculate(SpecificationChromosome) - Method in class geneticalgorithm.SpecificationFitness
calculateGenuineStatistics(List<Tlsf>, List<Tlsf>) - Static method in class main.AnalysisAgainstSpectra
calculateGenuineStatistics(List<Tlsf>, List<Tlsf>) - Static method in class main.GenuineSolutionsAnalysis
change_assert(Tlsf, List<Formula>) - Static method in class utils.TlsfUtils
change_assume(Tlsf, List<Formula>) - Static method in class utils.TlsfUtils
change_assume(Tlsf, Formula) - Static method in class utils.TlsfUtils
change_guarantees(Tlsf, List<Formula>) - Static method in class utils.TlsfUtils
change_guarantees(Tlsf, Formula) - Static method in class utils.TlsfUtils
change_initially(Tlsf, Formula) - Static method in class utils.TlsfUtils
change_preset(Tlsf, Formula) - Static method in class utils.TlsfUtils
change_require(Tlsf, Formula) - Static method in class utils.TlsfUtils
check_REALIZABILITY - Static variable in class main.Settings: Whether realisability (via Strix, or strong satisfiability when Settings.check_STRONG_SAT is set) is checked inside the fitness function itself, rather than only on final candidates (flag -onlySAT sets this to false; default true).
check_STRONG_SAT - Static variable in class main.Settings: Use the strong-satisfiability (potential realisability) check instead of a full Strix realisability query inside the fitness (flag -strongSAT, default false) — cheaper, less precise.
checkPotentiallyRealizability() - Method in class solvers.PotentiallyRealizabilityChecker
checkRealizability(String) - Static method in class solvers.StrixHelper: Parses the given TLSF text and checks its realisability.
checkRealizability(Spectra) - Static method in class solvers.StrixHelper: Checks the realisability of a Spectra specification object directly (as opposed to StrixHelper.checkRealizability(Tlsf)'s TLSF-to-Spectra conversion path): renders its formula to Strix syntax, extracts the input/output signal lists under the same contiguous-run convention described in the class documentation, and dispatches to StrixHelper.executeStrix(String, String, String).
checkRealizability(Tlsf) - Static method in class solvers.StrixHelper: Checks the realisability of a parsed TLSF specification.
checkStrongSatisfiable() - Method in class solvers.StrongSatisfiabilityChecker
clone() - Method in class geneticalgorithm.SpecificationChromosome: Shallow clone (the specification reference is shared, not copied).
combineSubformula(Formula, Formula) - Static method in class utils.FormulaUtils
compare(Formula, Formula) - Static method in class utils.FormulaUtils
compatible(SpecificationChromosome.SPEC_STATUS) - Method in enum geneticalgorithm.SpecificationChromosome.SPEC_STATUS: Whether two statuses can meaningfully be combined during the search: both must be computed and not completely broken, and the pair must not consist of two individuals broken on the same side.
compute_lost_models_porcentage(Tlsf, Tlsf) - Method in class geneticalgorithm.PreciseModelCountingSpecificationFitness
compute_semantic_distance(Tlsf, Tlsf) - Method in class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: Semantic similarity between two specifications, as the even average of the lost-models and won-models components: 0.5 * lost + 0.5 * won.
compute_status(SpecificationChromosome) - Method in class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: Computes and stores the SpecificationChromosome.SPEC_STATUS of a candidate, performing the satisfiability/realisability analysis that feeds the status ladder.
compute_status(SpecificationChromosome) - Method in class geneticalgorithm.ModelCountingSpecificationFitness
compute_status(SpecificationChromosome) - Method in class geneticalgorithm.PreciseModelCountingSpecificationFitness
compute_syntactic_distance(Tlsf, Tlsf) - Method in class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: Syntactic similarity between two specifications: the even average of the two sub-formula overlap ratios, 0.5 * |SF(S) ∩ SF(S')| / |SF(S)| + 0.5 * |SF(S) ∩ SF(S')| / |SF(S')|.
compute_syntactic_distance(Tlsf, Tlsf) - Method in class geneticalgorithm.ModelCountingSpecificationFitness
compute_syntactic_distance_size(Tlsf, Tlsf) - Method in class geneticalgorithm.ModelCountingSpecificationFitness
compute_syntactic_distance_size(Tlsf, Tlsf) - Method in class geneticalgorithm.PreciseModelCountingSpecificationFitness
compute_won_models_porcentage(Tlsf, Tlsf) - Method in class geneticalgorithm.PreciseModelCountingSpecificationFitness
computeFitness - Static variable in class main.GenuineSolutionsAnalysis
CONTRADICTORY - geneticalgorithm.SpecificationChromosome.SPEC_STATUS: Each side is satisfiable in isolation, but their conjunction is not.
count(int) - Method in class modelcounter.AutomataBasedModelCounting
count(int) - Method in class modelcounter.EmersonLeiAutomatonBasedModelCounting: Computes the approximate bounded model count #̂(formula, bound) = u * T^bound * v.
count(int) - Method in class modelcounter.MatrixBigIntegerModelCounting
count(long) - Method in class modelcounter.ABC
count(String, List<String>) - Method in class solvers.PreciseLTLModelCounter
count(LinkedList<String>, int, boolean, boolean) - Method in class modelcounter.ABC
count(List<LabelledFormula>, int, boolean, boolean) - Method in class modelcounter.CountREModels
count(Formula, int) - Method in class solvers.PreciseLTLModelCounter
count(LabelledFormula, int, boolean, boolean) - Method in class modelcounter.Count
Count - Class in modelcounter
Count() - Constructor for class modelcounter.Count
CountMain - Class in modelcounter
CountMain() - Constructor for class modelcounter.CountMain
countPrefixes(LabelledFormula, int) - Method in class modelcounter.CountRltlConv
CountREModels - Class in modelcounter
CountREModels() - Constructor for class modelcounter.CountREModels
CountRltlConv - Class in modelcounter
CountRltlConv() - Constructor for class modelcounter.CountRltlConv
createMatrix(int, int) - Method in class modelcounter.EmersonLeiAutomatonBasedModelCounting: Creates a zero matrix of the given dimensions with exact BigFraction entries.
createMatrix(int, int) - Method in class modelcounter.MatrixBigIntegerModelCounting
crossover(SpecificationChromosome) - Method in class geneticalgorithm.SpecificationChromosome: Recombines this individual with another parent, producing offspring that mix assumptions and guarantees from both.

D

dfaToGraph(Automaton) - Static method in class modelcounter.Buchi2Graph

E

EmersonLeiAutomatonBasedModelCounting<S> - Class in modelcounter: 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.
EmersonLeiAutomatonBasedModelCounting(LabelledFormula) - Constructor for class modelcounter.EmersonLeiAutomatonBasedModelCounting: Creates a counter for the given formula and immediately translates it into its Emerson-Lei automaton.
encoded_alphabet - Variable in class modelcounter.Rltlconv_LTLModelCounter
encoded_alphabet - Variable in class utils.Formula2Automaton
encoded_alphabet - Variable in class utils.FormulaToRE
equals(Object) - Method in class geneticalgorithm.SpecificationChromosome: Semantic-leaning equality used to deduplicate candidates (e.g.
equals(Tlsf, Tlsf) - Static method in class utils.TlsfUtils
ERROR - solvers.LTLSolver.SolverResult
ERROR - solvers.StrixHelper.RealizabilitySolverResult: Strix reported an error, or wrote to stderr, or exited abnormally.
executeStrix(String) - Static method in class solvers.StrixHelper: Runs the Spectra CLI on an already-written .spectra file, dispatching on Settings.USE_DOCKER.
executeStrix(String, String, String) - Static method in class solvers.StrixHelper: Runs the configured realisability/synthesis tool (Settings.SYNTH_TOOL, flag -synth) on an LTL formula plus explicit input/output signal lists, and returns its verdict.

F

finalExecutionTime - Variable in class geneticalgorithm.SpecificationGeneticAlgorithm: Timestamp taken at the very end of the run, after solutions have been printed.
fitness - Variable in class geneticalgorithm.SpecificationChromosome: Cached fitness value, filled in when the chromosome is evaluated.
Formula2Automaton<S> - Class in utils
Formula2Automaton() - Constructor for class utils.Formula2Automaton
FormulaMutator - Class in owl.ltl.visitors
FormulaMutator(List<String>, int, int) - Constructor for class owl.ltl.visitors.FormulaMutator
formulaSize(Formula) - Static method in class utils.FormulaUtils
FormulaStrengthening - Class in owl.ltl.visitors: The strengthening mutation mode of AuRUS: rewrites an LTL formula (in negation normal form) into a semantically stronger one, i.e.
FormulaStrengthening(List<String>, int, int) - Constructor for class owl.ltl.visitors.FormulaStrengthening: Creates a strengthening visitor over the given variable alphabet.
formulaToDfa(LabelledFormula) - Method in class utils.Formula2Automaton
FormulaToRE - Class in utils
FormulaToRE() - Constructor for class utils.FormulaToRE
formulaToRegularExpression(LabelledFormula) - Method in class utils.FormulaToRE
FormulaUtils - Class in utils
FormulaUtils() - Constructor for class utils.FormulaUtils
FormulaWeakening - Class in owl.ltl.visitors: The weakening mutation mode of AuRUS: rewrites an LTL formula (in negation normal form) into a semantically weaker one, i.e.
FormulaWeakening(List<String>, int, int) - Constructor for class owl.ltl.visitors.FormulaWeakening: Creates a weakening visitor over the given variable alphabet.
fromSpec(Tlsf) - Static method in class utils.TlsfUtils
fromSpectra(Spectra) - Static method in class utils.TlsfUtils

G

GA_CROSSOVER_RATE - Static variable in class main.Settings: Percentage of chromosomes selected for crossover at each generation (flag -COR, default 10).
GA_EXECUTION_TIMEOUT - Static variable in class main.Settings: Overall wall-clock budget for the genetic search, in seconds (flag -GATO, default 0 — no timeout).
GA_GENE_MUTATION_RATE - Static variable in class main.Settings: Probability (%) with which each gene (sub-formula) of a mutated chromosome is itself mutated (flag -geneMR, default 0).
GA_GENE_NUM_OF_MUTATIONS - Static variable in class main.Settings: Maximum number of genes (sub-formulas) mutated per formula (flag -geneNUM, default 0).
GA_GENERATIONS - Static variable in class main.Settings: Number of generations the search runs for (flag -Gen, default 10).
GA_GUARANTEES_PREFERENCE_FACTOR - Static variable in class main.Settings: Probability (%, p) that a genetic operator (mutation or crossover) targets the guarantees rather than the assumptions; the assumptions are targeted with probability 1-p (flag -GPR, default 50).
GA_MAX_NUM_INDIVIDUALS - Static variable in class main.Settings: Hard cap on the total number of individuals ever generated, across all generations (flag -Max, default: unbounded).
GA_MUTATION_RATE - Static variable in class main.Settings: Probability (%) with which the mutation operator is applied to each chromosome (flag -MR, default 100 — always).
GA_POPULATION_SIZE - Static variable in class main.Settings: Population size retained at each generation (flag -Pop, default 100).
GA_RANDOM_SELECTOR - Static variable in class main.Settings: Use a random selector instead of the best-selector for the next generation's parents (flag -GA_random_selector, default false).
GA_REMOVE_ASSUMPTION_PROB - Static variable in class main.Settings: Probability (in %) that the mutation operator drops an assumption conjunct entirely instead of rewriting one of its sub-formulas, when allowAssumptionRemoval is enabled (flag -removeAProb, default 5).
GA_REMOVE_GUARANTEE_PROB - Static variable in class main.Settings: Probability (in %) that the mutation operator drops a guarantee conjunct entirely instead of rewriting one of its sub-formulas, when allowGuaranteeRemoval is enabled (flag -removeGProb, default 0).
GA_THRESHOLD - Static variable in class main.Settings: Minimum fitness a candidate must reach to be collected as a solution during the search (flag -sol, default 0.0 — no threshold).
GANAK - solvers.PreciseLTLModelCounter.MODEL_COUNTER
genABCString(LabelledFormula) - Method in class modelcounter.Count
genABCString(LabelledFormula) - Method in class modelcounter.CountREModels
genAlphabet(int) - Static method in class utils.SolverUtils
GeneralFormulaMutator - Class in owl.ltl.visitors
GeneralFormulaMutator(List<String>, int, int) - Constructor for class owl.ltl.visitors.GeneralFormulaMutator
generateLabels(Nba) - Method in class modelcounter.Rltlconv_LTLModelCounter
generateLabels(List<String>) - Method in class utils.Formula2Automaton
generateLabels(List<String>) - Method in class utils.FormulaToRE
geneticalgorithm - package geneticalgorithm
genRltlString(LabelledFormula) - Method in class modelcounter.CountRltlConv
GenuineSolutionsAnalysis - Class in main
GenuineSolutionsAnalysis() - Constructor for class main.GenuineSolutionsAnalysis
genuineSolutionsFound - Static variable in class main.GenuineSolutionsAnalysis
getCommand() - Method in class solvers.PreciseLTLModelCounter
getFormulaWOGFpattern(Formula) - Static method in class utils.TlsfUtils
getNode(Graph<String>, String) - Static method in class modelcounter.Buchi2Graph
getNumber(String) - Method in enum solvers.PreciseLTLModelCounter.MODEL_COUNTER
GUARANTEES - geneticalgorithm.SpecificationChromosome.SPEC_STATUS: The guarantees are satisfiable, but the assumptions are not (vacuous realisability).

H

hasGFPattern(Formula) - Static method in class utils.TlsfUtils
hashCode() - Method in class geneticalgorithm.SpecificationChromosome: Hash consistent with SpecificationChromosome.equals(Object), combining the specification, the status and the fitness.

I

inconclusive() - Method in enum solvers.LTLSolver.SolverResult
inconclusive() - Method in enum solvers.StrixHelper.RealizabilitySolverResult
INFILE - Variable in class solvers.PreciseLTLModelCounter
initialExecutionTime - Variable in class geneticalgorithm.SpecificationGeneticAlgorithm: Timestamp taken when the run starts, before building the initial population.
isSAT(String) - Static method in class solvers.LTLSolver
isSpecificationConsistent() - Method in enum geneticalgorithm.SpecificationChromosome.SPEC_STATUS
isStrongSatisfiable(LabelledFormula) - Method in class solvers.StrongSATSolver

L

labelIDs - Variable in class modelcounter.Rltlconv_LTLModelCounter
labelIDs - Variable in class utils.Formula2Automaton
labelIDs - Variable in class utils.FormulaToRE
lessGeneralSolutions - Static variable in class main.GenuineSolutionsAnalysis
LOST_MODELS_FACTOR - Static variable in class main.Settings: Weight of the lost-models direction of the semantic-similarity component (half of γ from -factors; default 0.1).
LTL2Graph(LabelledFormula) - Static method in class modelcounter.Buchi2Graph
ltl2nba(String) - Method in class modelcounter.Rltlconv_LTLModelCounter
ltl2RE(String) - Method in class modelcounter.Rltlconv_LTLModelCounter
LTLSolver - Class in solvers
LTLSolver() - Constructor for class solvers.LTLSolver
LTLSolver.SolverResult - Enum in solvers

M

main - package main
main(String[]) - Static method in class main.AnalysisAgainstSpectra
main(String[]) - Static method in class main.GenuineSolutionsAnalysis
main(String[]) - Static method in class main.Main: Parses the arguments, configures Settings, runs the search and writes the repairs and the summary report.
main(String[]) - Static method in class main.ModelCountingRanking
main(String[]) - Static method in class main.PreciseModelCountingEvaluation
main(String[]) - Static method in class main.SynSemDistanceAnalysis
main(String[]) - Static method in class main.TestRunner
main(String[]) - Static method in class main.WellSeparationAnalysis
main(String[]) - Static method in class modelcounter.CountMain
Main - Class in main: Command-line entry point of AuRUS.
Main() - Constructor for class main.Main
MatrixBigIntegerModelCounting - Class in modelcounter
MatrixBigIntegerModelCounting(LabelledFormula, boolean) - Constructor for class modelcounter.MatrixBigIntegerModelCounting
MAX_FITNESS() - Static method in class main.Settings: Theoretical maximum value the fitness function can return: the sum of all four component weights.
MC_BOUND - Static variable in class main.Settings: Bound k for the bounded model-counting approach (flag -k, default 10).
MC_EXHAUSTIVE - Static variable in class main.Settings: Intended to select an exact model counter instead of the automata/matrix approximation (flag -precise sets this to false; default true).
MC_TIMEOUT - Static variable in class main.Settings: Timeout, in seconds, for a single bounded model-counting query (flag -MCTO, default 180).
merge(Tlsf, Tlsf) - Static method in class geneticalgorithm.SpecificationMerger
merge(Tlsf, Tlsf, SpecificationChromosome.SPEC_STATUS, SpecificationChromosome.SPEC_STATUS, int) - Static method in class geneticalgorithm.SpecificationMerger
MINIC2D - solvers.PreciseLTLModelCounter.MODEL_COUNTER
modelcounter - package modelcounter
modelcounter - Variable in class solvers.PreciseLTLModelCounter
ModelCountingRanking - Class in main
ModelCountingRanking() - Constructor for class main.ModelCountingRanking
ModelCountingSpecificationFitness - Class in geneticalgorithm
ModelCountingSpecificationFitness(Tlsf) - Constructor for class geneticalgorithm.ModelCountingSpecificationFitness
moreGeneralSolutions - Static variable in class main.GenuineSolutionsAnalysis
mutate() - Method in class geneticalgorithm.SpecificationChromosome: Produces a mutated copy of this individual by delegating to SpecificationMutator, which selects an assumption or a guarantee (biased by -GPR), picks a random sub-formula inside it, and rewrites it with one of the three mutation modes (general, weakening, strengthening).
mutate(Tlsf) - Static method in class geneticalgorithm.SpecificationMutator: Applies the three-step mutation operator described in the class documentation to the given specification.

N

nbaToDfa(Automaton<S, ? extends OmegaAcceptance>) - Method in class utils.Formula2Automaton
new_literal(Formula) - Method in class owl.ltl.visitors.FormulaStrengthening: Picks a literal, from the specification's variable alphabet, to combine with a formula being strengthened.
new_literal(Formula) - Method in class owl.ltl.visitors.FormulaWeakening: Picks a literal, from the specification's variable alphabet, to combine with a formula being weakened — used by the "add disjunct" / "widen the until" style rules above.
new_literal(Formula) - Method in class owl.ltl.visitors.GeneralFormulaMutator
numOfAllowedMutations - Variable in class owl.ltl.visitors.FormulaMutator
numOfAllowedMutations - Variable in class owl.ltl.visitors.GeneralFormulaMutator
numOfCalls - Static variable in class solvers.LTLSolver
numOfCalls - Variable in class solvers.PreciseLTLModelCounter
numOfError - Static variable in class solvers.LTLSolver
numOfError - Variable in class solvers.PreciseLTLModelCounter
numOfTemporalOperators(Formula) - Static method in class utils.FormulaUtils
numOfTimeout - Static variable in class solvers.LTLSolver
numOfTimeout - Variable in class solvers.PreciseLTLModelCounter

O

only_inputs_in_assumptions - Static variable in class main.Settings: Restrict newly generated/transplanted assumption fragments to input variables only (flag -onlyInputsA, default false), preventing the environment from being "repaired" with constraints over outputs it cannot observe.
originalNegationNumOfModels - Variable in class geneticalgorithm.PreciseModelCountingSpecificationFitness
originalNumOfModels - Variable in class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: Bounded model count #(S, k) of the original specification, computed once at construction time (only when the lost-models component is active).
originalNumOfModels - Variable in class geneticalgorithm.ModelCountingSpecificationFitness
originalNumOfModels - Variable in class geneticalgorithm.PreciseModelCountingSpecificationFitness
originalSpecification - Variable in class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: The original (typically unrealisable) specification every candidate is compared against.
originalSpecification - Variable in class geneticalgorithm.ModelCountingSpecificationFitness
originalSpecification - Variable in class geneticalgorithm.PreciseModelCountingSpecificationFitness
originalStatus - Variable in class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: Status of the original specification, computed once at construction time.
originalStatus - Variable in class geneticalgorithm.ModelCountingSpecificationFitness
originalStatus - Variable in class geneticalgorithm.PreciseModelCountingSpecificationFitness
owl.ltl.visitors - package owl.ltl.visitors

P

PARSING_TIMEOUT - Static variable in class main.Settings: Timeout, in seconds, for translating a formula into its automaton (default 60).
PAtoDfa(Automaton<S, ParityAcceptance>) - Method in class utils.Formula2Automaton
PotentiallyRealizabilityChecker<S> - Class in solvers
PotentiallyRealizabilityChecker(LabelledFormula) - Constructor for class solvers.PotentiallyRealizabilityChecker
PreciseLTLModelCounter - Class in solvers
PreciseLTLModelCounter() - Constructor for class solvers.PreciseLTLModelCounter
PreciseLTLModelCounter.MODEL_COUNTER - Enum in solvers
PreciseModelCountingEvaluation - Class in main
PreciseModelCountingEvaluation() - Constructor for class main.PreciseModelCountingEvaluation
PreciseModelCountingSpecificationFitness - Class in geneticalgorithm
PreciseModelCountingSpecificationFitness(Tlsf) - Constructor for class geneticalgorithm.PreciseModelCountingSpecificationFitness
print_config() - Method in class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: Prints the active fitness configuration to standard output: the four component weights (status, lost models, won models, syntactic) and the assumption-addition / guarantee-removal flags.
print_config() - Method in class geneticalgorithm.SpecificationGeneticAlgorithm: Returns a one-line summary of the current genetic-algorithm configuration: generations, population size, individuals budget, mutation rate and crossover rate.
print_execution_time() - Method in class geneticalgorithm.SpecificationGeneticAlgorithm: Returns a summary of the wall-clock time spent by the run: the search time (initial population until the end of the evolution) and the total time (until solutions were printed), both in seconds.
print_settings() - Static method in class main.Settings: Serialises every setting relevant to reproducing a run into a single line, printed at the start and end of Main and written to out.txt.
printMatrix(FieldMatrix<BigFraction>) - Method in class modelcounter.EmersonLeiAutomatonBasedModelCounting: Debug helper: prints a matrix to standard output, one row per line.
PropositionVariablesExtractor - Class in owl.ltl.visitors
PropositionVariablesExtractor() - Constructor for class owl.ltl.visitors.PropositionVariablesExtractor

R

RANDOM_GENERATOR - Static variable in class main.Settings: Shared random source for every stochastic decision in the search (selection coin flips, mutation targets, ...), seeded from Settings.SEED.
REALIZABLE - geneticalgorithm.SpecificationChromosome.SPEC_STATUS: The specification is consistent and realisable — a repair.
REALIZABLE - solvers.StrixHelper.RealizabilitySolverResult: A controller exists: the specification is realisable.
RELSAT - solvers.PreciseLTLModelCounter.MODEL_COUNTER
removeSameGuarantees(List<Tlsf>) - Static method in class main.AnalysisAgainstSpectra
replaceSubformula(Formula, Formula) - Static method in class utils.FormulaUtils
result - Variable in class modelcounter.ABC
Rltlconv_LTLModelCounter - Class in modelcounter
Rltlconv_LTLModelCounter() - Constructor for class modelcounter.Rltlconv_LTLModelCounter
run(Tlsf) - Method in class geneticalgorithm.SpecificationGeneticAlgorithm: Runs the genetic search on the given specification using the fitness weights currently configured in Settings (equivalent to calling SpecificationGeneticAlgorithm.run(Tlsf, double, double, double) with negative factors, which leaves the configured values untouched).
run(Tlsf, double, double, double) - Method in class geneticalgorithm.SpecificationGeneticAlgorithm: Runs the complete genetic search on the given specification.
runRandom(Tlsf) - Method in class geneticalgorithm.SpecificationGeneticAlgorithm: Baseline used in the experimental evaluation (flag -random): instead of evolving the population, it generates Settings.GA_POPULATION_SIZE random mutants of the input specification and checks each one for realisability with Strix at the end.

S

SAT - solvers.LTLSolver.SolverResult
SAT_TIMEOUT - Static variable in class main.Settings: Timeout, in seconds, for a single LTL satisfiability query (flag -SatTO, default 30).
searchExecutionTime - Variable in class geneticalgorithm.SpecificationGeneticAlgorithm: Timestamp taken when the evolutionary search finishes (before the final realisability sweep).
SEED - Static variable in class main.Settings: The seed backing Settings.RANDOM_GENERATOR.
semantic_distance - Variable in class geneticalgorithm.SpecificationChromosome: Cached semantic similarity to the original specification, in [0, 1].
setFactors(double, double, double) - Static method in class main.Settings: Sets the three top-level fitness weights (realisability status, syntactic similarity, semantic similarity), splitting the semantic weight evenly between Settings.LOST_MODELS_FACTOR and Settings.WON_MODELS_FACTOR.
setLabel(String) - Method in class modelcounter.Rltlconv_LTLModelCounter
setLabel(String) - Method in class utils.Formula2Automaton
setLabel(String) - Method in class utils.FormulaToRE
setLabelEncoded(String) - Method in class modelcounter.Rltlconv_LTLModelCounter
setLabelEncoded(String) - Method in class utils.Formula2Automaton
setLabelEncoded(String) - Method in class utils.FormulaToRE
setStrixName(String) - Static method in class main.Settings: Redirects Settings.STRIX_PATH to the given output directory (called when -out is supplied), so Strix's temporary files land next to the repairs rather than in the default docker/ directory.
Settings - Class in main: Central, static configuration of AuRUS: every knob the genetic search, the fitness function, the model counter and the external solvers read from.
Settings() - Constructor for class main.Settings
solution() - Method in enum solvers.PreciseLTLModelCounter.MODEL_COUNTER
solutions - Variable in class geneticalgorithm.SpecificationGeneticAlgorithm: Realisable repairs found during the search, i.e.
solvers - package solvers
SolverSyntaxOperatorReplacer - Class in owl.ltl.visitors
SolverSyntaxOperatorReplacer() - Constructor for class owl.ltl.visitors.SolverSyntaxOperatorReplacer
SolverUtils - Class in utils
SolverUtils() - Constructor for class utils.SolverUtils
somethingHasBeenRemoved(Tlsf, Tlsf) - Method in class geneticalgorithm.AutomataBasedModelCountingSpecificationFitness: Structural guard used to prune candidates that transgress the configured search space: returns true if the candidate added an assumption while Settings.allowAssumptionAddition is disabled, or removed a guarantee while Settings.allowGuaranteeRemoval is disabled (both detected by comparing conjunct counts against the original specification).
spec - Variable in class geneticalgorithm.SpecificationChromosome: The assume-guarantee specification this individual represents.
SpecificationChromosome - Class in geneticalgorithm: The individual of AuRUS's genetic search: a complete assume-guarantee specification, together with its cached evaluation results.
SpecificationChromosome() - Constructor for class geneticalgorithm.SpecificationChromosome: Creates an empty chromosome with no specification (used internally).
SpecificationChromosome(Tlsf) - Constructor for class geneticalgorithm.SpecificationChromosome: Creates a chromosome for the given specification.
SpecificationChromosome.SPEC_STATUS - Enum in geneticalgorithm: The evaluation lattice of a candidate specification, ordered from completely broken to repaired:
SpecificationCrossover - Class in geneticalgorithm: 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.
SpecificationCrossover() - Constructor for class geneticalgorithm.SpecificationCrossover
SpecificationFitness - Class in geneticalgorithm
SpecificationFitness() - Constructor for class geneticalgorithm.SpecificationFitness
SpecificationGeneticAlgorithm - Class in geneticalgorithm: Main entry point of the AuRUS search: a genetic algorithm that evolves candidate repairs for an unrealisable assume-guarantee LTL specification.
SpecificationGeneticAlgorithm() - Constructor for class geneticalgorithm.SpecificationGeneticAlgorithm
SpecificationMerger - Class in geneticalgorithm
SpecificationMerger() - Constructor for class geneticalgorithm.SpecificationMerger
SpecificationMutator - Class in geneticalgorithm: 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.
SpecificationMutator() - Constructor for class geneticalgorithm.SpecificationMutator
SPECTRA_PATH - Static variable in class main.Settings: Working directory used when checking realisability of Spectra specifications (-use-spectra, default "docker-spectra/").
splitConjunction(Formula) - Static method in class utils.FormulaUtils
splitConjunction(LabelledFormula) - Static method in class utils.FormulaUtils
splitConjunctions(List<Formula>) - Static method in class utils.FormulaUtils
state - Variable in class modelcounter.Rltlconv_LTLModelCounter
state - Variable in class utils.Formula2Automaton
state - Variable in class utils.FormulaToRE
status - Variable in class geneticalgorithm.SpecificationChromosome: Cached realisability status, computed lazily by the fitness function.
STATUS_FACTOR - Static variable in class main.Settings: Weight α of the realisability-status component in the fitness sum (flag -factors, first value; default 0.7).
strengthenFormula(Formula, List<String>) - Static method in class geneticalgorithm.SpecificationMutator: Applies the semantically directed strengthening mutation, producing a formula φ_s such that φ_s ⊨ φ: no new model is introduced (e.g.
STRIX_PATH - Static variable in class main.Settings: Working directory Strix (native or Docker) reads/writes its temporary TLSF files in; overridden to the output directory via Settings.setStrixName(java.lang.String) when -out is given (default "docker/").
STRIX_TIMEOUT - Static variable in class main.Settings: Timeout, in seconds, for a single Strix realisability query (flag -RTO, default 20).
StrixHelper - Class in solvers: 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() - Constructor for class solvers.StrixHelper
StrixHelper.RealizabilitySolverResult - Enum in solvers: Outcome of a Strix realisability query.
STRONG_SAT_TIMEOUT - Static variable in class main.Settings: Timeout, in seconds, for a strong-satisfiability query (default 180).
StrongSatisfiabilityChecker<S> - Class in solvers
StrongSatisfiabilityChecker(LabelledFormula) - Constructor for class solvers.StrongSatisfiabilityChecker
StrongSATSolver<S> - Class in solvers
StrongSATSolver() - Constructor for class solvers.StrongSATSolver
SubformulaReplacer - Class in owl.ltl.visitors: Replaces every occurrence of a given sub-formula with another, throughout an LTL formula's syntax tree.
SubformulaReplacer(Formula, Formula) - Constructor for class owl.ltl.visitors.SubformulaReplacer: Creates a replacer that will substitute every occurrence of source with target.
subformulas(Formula) - Static method in class utils.FormulaUtils
subformulas(LabelledFormula) - Static method in class utils.FormulaUtils
SynSemDistanceAnalysis - Class in main
SynSemDistanceAnalysis() - Constructor for class main.SynSemDistanceAnalysis
syntactic_distance - Variable in class geneticalgorithm.SpecificationChromosome: Cached syntactic similarity to the original specification, in [0, 1].
SYNTACTIC_FACTOR - Static variable in class main.Settings: Weight β of the syntactic-similarity component in the fitness sum (flag -factors, second value; default 0.1).
SYNTH_BIN - Static variable in class main.Settings: Path/name of the synthesiser binary to invoke for Settings.SYNTH_TOOL (flag -synth-bin).
SYNTH_TOOL - Static variable in class main.Settings: Which realisability/synthesis tool to invoke (flag -synth, default "strix").

T

telaToDfa(Automaton<S, EmersonLeiAcceptance>) - Method in class utils.Formula2Automaton
TestRunner - Class in main
TestRunner() - Constructor for class main.TestRunner
TIMEOUT - solvers.LTLSolver.SolverResult
TIMEOUT - solvers.StrixHelper.RealizabilitySolverResult: Strix did not answer within Settings.STRIX_TIMEOUT seconds.
TIMEOUT - Static variable in class modelcounter.AutomataBasedModelCounting
TIMEOUT - Variable in class modelcounter.CountRltlConv
TIMEOUT - Variable in class modelcounter.Rltlconv_LTLModelCounter
TIMEOUT - Variable in class solvers.PreciseLTLModelCounter
TLSF_EXAMPLE_SPEC - Static variable in class utils.TlsfUtils
tlsf2spectra(Tlsf) - Static method in class utils.TlsfUtils
TlsfUtils - Class in utils
TlsfUtils() - Constructor for class utils.TlsfUtils
toABClanguage(String) - Method in class modelcounter.CountREModels
toABClanguage(String) - Method in class modelcounter.Rltlconv_LTLModelCounter
toBasicTLSF(File) - Static method in class utils.TlsfUtils
toBasicTLSF(String) - Static method in class utils.TlsfUtils
toLambConvSyntax(String) - Static method in class utils.SolverUtils
toSolverSyntax(String) - Static method in class utils.SolverUtils
toSolverSyntax(Formula) - Static method in class utils.SolverUtils
toSolverSyntax(LabelledFormula) - Static method in class utils.SolverUtils
toString() - Method in enum geneticalgorithm.SpecificationChromosome.SPEC_STATUS
toString() - Method in enum solvers.PreciseLTLModelCounter.MODEL_COUNTER
toTLSF(Tlsf) - Static method in class utils.TlsfUtils

U

UNKNOWN - geneticalgorithm.SpecificationChromosome.SPEC_STATUS: The status of the specification has not been computed yet.
UNREALIZABLE - geneticalgorithm.SpecificationChromosome.SPEC_STATUS: The specification is consistent, but no controller can realise it.
UNREALIZABLE - solvers.StrixHelper.RealizabilitySolverResult: No controller exists: the specification is unrealisable.
UNSAT - solvers.LTLSolver.SolverResult
USE_DOCKER - Static variable in class main.Settings: Run Strix through the Docker image rather than the local install (flags -docker/-no-docker, default false — native).
USE_SPECTRA - Static variable in class main.Settings: Treat the input as a Spectra specification instead of TLSF (flag -use-spectra, default false).
utils - package utils

V

valueOf(String) - Static method in enum geneticalgorithm.SpecificationChromosome.SPEC_STATUS: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum solvers.LTLSolver.SolverResult: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum solvers.PreciseLTLModelCounter.MODEL_COUNTER: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum solvers.StrixHelper.RealizabilitySolverResult: Returns the enum constant of this type with the specified name.
values() - Static method in enum geneticalgorithm.SpecificationChromosome.SPEC_STATUS: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum solvers.LTLSolver.SolverResult: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum solvers.PreciseLTLModelCounter.MODEL_COUNTER: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum solvers.StrixHelper.RealizabilitySolverResult: Returns an array containing the constants of this enum type, in the order they are declared.
variables() - Method in class owl.ltl.visitors.FormulaMutator
variables() - Method in class owl.ltl.visitors.FormulaStrengthening
variables() - Method in class owl.ltl.visitors.FormulaWeakening
visit(Biconditional) - Method in class owl.ltl.visitors.FormulaMutator
visit(Biconditional) - Method in class owl.ltl.visitors.FormulaStrengthening: Rejected: the mutator only ever runs on formulas already converted to negation normal form.
visit(Biconditional) - Method in class owl.ltl.visitors.FormulaWeakening: Rejected: the mutator only ever runs on formulas already converted to negation normal form.
visit(Biconditional) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(Biconditional) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(Biconditional) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(Biconditional) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into both operands.
visit(BooleanConstant) - Method in class owl.ltl.visitors.FormulaMutator
visit(BooleanConstant) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens a boolean constant: true ⤳ false (the only possible strengthening of a constant; false is already the strongest formula and is left untouched by the random draw).
visit(BooleanConstant) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens a boolean constant: false ⤳ true (the only possible weakening of a constant; true is already the weakest formula and is left untouched by the random draw).
visit(BooleanConstant) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(BooleanConstant) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(BooleanConstant) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(BooleanConstant) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; a boolean constant has no children to recurse into.
visit(Conjunction) - Method in class owl.ltl.visitors.FormulaMutator
visit(Conjunction) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens a conjunction a1 ∧ ... ∧ an (recursing into every conjunct first) into one of: false (option 0); adding one more conjunct drawn from the alphabet, a1 ∧ a2 ⤳ a1 ∧ a2 ∧ c (option 1 — a conjunction can only become more demanding by adding conjuncts); or, when not already temporally heavy, G(a1 ∧ ... ∧ an) (option 2 — requiring the whole conjunction to hold forever rather than just now).
visit(Conjunction) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens a conjunction a1 ∧ ... ∧ an (recursing into every conjunct first) into one of: true (option 0); dropping one randomly chosen conjunct, a1 ∧ a2 ⤳ a1 (option 1 — Table 4.1's "drop conjunct" rule); turning the whole conjunction into a disjunction, a1 ∧ a2 ⤳ a1 ∨ a2 (option 2); or, when the formula is not already temporally heavy, F(a1 ∧ ... ∧ an) (option 3 — postponing the whole conjunction rather than requiring it now).
visit(Conjunction) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(Conjunction) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(Conjunction) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(Conjunction) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into every conjunct.
visit(Disjunction) - Method in class owl.ltl.visitors.FormulaMutator
visit(Disjunction) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens a disjunction a1 ∨ ... ∨ an (recursing into every disjunct first) into one of: false (option 0); turning the whole disjunction into a conjunction, a1 ∨ a2 ⤳ a1 ∧ a2 (option 1 — Table 4.1's "conjunct" rule); dropping one randomly chosen disjunct, a1 ∨ a2 ⤳ a1 (option 2 — narrowing which alternative is allowed); or, when not already temporally heavy, G(a1 ∨ ... ∨ an) (option 3 — requiring the disjunction to hold forever rather than just now).
visit(Disjunction) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens a disjunction a1 ∨ ... ∨ an (recursing into every disjunct first) into one of: true (option 0); or adding one more disjunct drawn from the alphabet, a1 ∨ a2 ⤳ a1 ∨ a2 ∨ c (option 1 — a disjunction can only grow more permissive by adding disjuncts).
visit(Disjunction) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(Disjunction) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(Disjunction) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(Disjunction) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into every disjunct.
visit(FOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(FOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens F(a) (recursing into a first) into one of, drawn uniformly out of 8 outcomes: false (option 0); a itself (option 1 — requiring it now rather than eventually); X(a) (option 2 — requiring it at the very next step); G(a) (option 3 — requiring it forever, Table 4.1's strongest "eventually" tightening); F X(a) (option 4, guarded against runaway size — delaying by exactly one step); F G(a) (option 5, same guard — "eventually always", strictly implying plain "eventually"); G F(a) (option 6, same guard — "infinitely often" is the valid strengthening direction of "eventually always", the mirror of FormulaWeakening.visit(GOperator)'s weakening of G F down to F G); or a U b for a drawn literal b (option 7 — requiring a to hold at least until some point, rather than merely eventually).
visit(FOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens F(a) (recursing into a first) into one of, drawn uniformly out of 6 outcomes: true (option 0, default); distributing over a conjunction, F(a1 ∧ a2) ⤳ F(a1) ∧ F(a2) (option 1, only when a is a conjunction — each conjunct is allowed to happen at its own time rather than simultaneously); F G(b) ⤳ G F(b) (option 2, when a = G(b) — the classic valid LTL implication "eventually always" ⇒ "infinitely often"); F X(b) ⤳ F(b) (option 3, when a = X(b) — dropping the extra step of delay); F G(b) ⤳ F(b) (option 4, when a = G(b) — a second, independent weakening applicable to the same F G(b) shape as option 2, this one discarding the "forever" and keeping only the first occurrence); or, as the fallback for every other case, F(a) ⤳ (c W a) for a drawn literal c (option 5 and any option whose structural guard failed) — see the class-level caveat about this fallback's soundness.
visit(FOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(FOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(FOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(FOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into the operand.
visit(FrequencyG) - Method in class owl.ltl.visitors.FormulaMutator
visit(FrequencyG) - Method in class owl.ltl.visitors.FormulaStrengthening: Rejected: the mutator only ever runs on formulas already converted to negation normal form.
visit(FrequencyG) - Method in class owl.ltl.visitors.FormulaWeakening: Rejected: the mutator only ever runs on formulas already converted to negation normal form.
visit(FrequencyG) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(FrequencyG) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(FrequencyG) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(FrequencyG) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into the operand.
visit(GOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(GOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens G(a) (recursing into a first) into one of, drawn uniformly out of 5 outcomes: false (option 0, default); distributing over a disjunction, G(a1 ∨ a2) ⤳ G(a1) ∨ G(a2) (option 1, only when a is a disjunction, via the disjunctive normal form of the operand — each disjunct is required to hold forever on its own, rather than the weaker requirement that some disjunct hold at each step); G F(b) ⤳ F G(b) (option 2, when a = F(b) — the valid strengthening direction noted above); simplifying G X(b) down to G(b) (option 3, when a = X(b) — equivalent, since "always" already covers the next step); or simplifying the (already-idempotent) G G(b) down to G(b) (option 4, when a is itself a G-formula — a non-strict, equivalence-preserving simplification rather than a proper strengthening).
visit(GOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens G(a) (recursing into a first) into one of, drawn uniformly out of 7 outcomes: true (option 0); a itself (option 1 — dropping "always" entirely, Table 4.1's "identity" row); F(a) (option 2 — "always" implies "eventually"); X(a) (option 3 — "always" implies "next"); G F(a) (option 4, only when the formula so far has at most one other temporal operator — "always" implies "infinitely often"); F G(a) (option 5, same guard — "always" implies "eventually always", the classic valid direction); or X G(a) (option 6 — delaying the "always" by one step is itself a weakening).
visit(GOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(GOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(GOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(GOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into the operand.
visit(HOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(HOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
visit(HOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
visit(HOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(HOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(HOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(HOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into the operand (past-time "historically").
visit(Literal) - Method in class owl.ltl.visitors.FormulaMutator
visit(Literal) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens an atomic literal p into one of, chosen uniformly at random: false (option 0); p ∧ q for a fresh literal q (option 1 — Table 4.1's "add conjunct" rule); or G(p) (option 2 — "always" is stronger than "now").
visit(Literal) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens an atomic literal p into one of, chosen uniformly at random: true (option 0); p ∨ q for a fresh literal q (option 1 — Table 4.1's "add disjunct" rule); or F(p) (option 2 — "eventually" is weaker than "now").
visit(Literal) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(Literal) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(Literal) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(Literal) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this literal matches SubformulaReplacer.source; a literal has no children to recurse into.
visit(MOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(MOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens a M b ("strong release" — via the standard duality a M b ≡ b U (a ∧ b), and its own unrolling ≡ (a ∧ b) ∨ (b ∧ ¬(a ∧ b) ∧ X(b U (a ∧ b))) — recursing into both sides first) into one of: false (option 0); a ∧ b (option 1 — requiring the joint condition to hold now, the strongest immediate reading); or b ∧ ¬(a ∧ b) ∧ X(a M b) (option 2 — unrolling one step of the "strong release" obligation).
visit(MOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens a M b ("strong release" — via the standard duality a M b ≡ b U (a ∧ b) — recursing into both sides first) into one of: true (option 0); b W (a ∧ b) (option 1 — the weak-until relaxation of the duality above, dropping the requirement that a ∧ b eventually hold); or F(a ∧ b) (option 2 — keeping only the eventual joint obligation).
visit(MOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(MOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(MOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(MOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into both operands ("strong release").
visit(OOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(OOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Rejected: the mutator only ever runs on formulas already converted to negation normal form.
visit(OOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Rejected: the mutator only ever runs on formulas already converted to negation normal form.
visit(OOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(OOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(OOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(OOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into the operand (past-time "once").
visit(ROperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(ROperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens a R b ("release" — via the standard duality a R b ≡ b W (a ∧ b) ≡ G(b) ∨ (a M b) — recursing into both sides first) into one of: false (option 0); G(b) (option 1 — keeping only the "always b" disjunct); or a M b (option 2 — keeping only the "strong release" disjunct, strictly stronger than the original release).
visit(ROperator) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens a R b ("release" — via the standard duality a R b ≡ b W (a ∧ b) — recursing into both sides first) into one of: true (option 0); F(b) ∨ (b U (a ∧ b)) (option 1 — relaxing the "always b" disjunct of the weak-until expansion down to a bare "eventually b"); or G(b) ∨ F(a ∧ b) (option 2 — relaxing the "until" disjunct down to a bare "eventually" joint obligation).
visit(ROperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(ROperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(ROperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(ROperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into both operands ("release").
visit(SOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(SOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
visit(SOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
visit(SOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(SOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(SOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(SOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into both operands (past-time "since").
visit(TOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(TOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
visit(TOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
visit(TOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(TOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(TOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(TOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into both operands (past-time "trigger").
visit(UOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(UOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens a U b (recursing into both sides first) via its unrolling a U b ≡ b ∨ (a ∧ ¬b ∧ X(a U b)), into one of: false (option 0); b (option 1 — requiring the eventual condition to hold now, dropping the "until" build-up entirely); or, when not already temporally heavy, a ∧ ¬b ∧ X(a U b) (option 2 — unrolling one step: a must hold now, b must not yet, and the same obligation continues from the next step).
visit(UOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens a U b ("a holds until b", recursing into both sides first) into one of: true (option 0); a W b (option 1 — the weak-until Table 4.1 rule: b no longer needs to eventually hold); (a ∨ c) U b for a drawn literal c (option 2 — widening what may hold while waiting for b); or F(b) (option 3 — keeping only the eventual obligation, dropping the "until" precondition on a).
visit(UOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(UOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(UOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(UOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into both operands ("until").
visit(WOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(WOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens a W b (recursing into both sides first).
visit(WOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens a W b ("a holds unless/until b", recursing into both sides first).
visit(WOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(WOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(WOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(WOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into both operands ("weak until").
visit(XOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(XOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Strengthens X(a) (recursing into a first) into one of: false (option 0, default); G(a) (option 1 — "always" from the next step on is stronger than a single "next"); or, when a is itself G(b), simplifying X G(b) down to G(b) (option 2 — equivalent, since "always from the next step" already implies "always").
visit(XOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Weakens X(a) (recursing into a first) into one of: true (option 0, default); F(a) (option 1 — dropping the "next" timing keeps only "eventually"); or, when a is itself F(b), simplifying X F(b) down to F(b) (option 2 — "eventually" already absorbs one step of delay).
visit(XOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(XOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(XOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(XOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into the operand ("next").
visit(YOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(YOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
visit(YOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
visit(YOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(YOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(YOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(YOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into the operand (past-time "yesterday").
visit(ZOperator) - Method in class owl.ltl.visitors.FormulaMutator
visit(ZOperator) - Method in class owl.ltl.visitors.FormulaStrengthening: Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
visit(ZOperator) - Method in class owl.ltl.visitors.FormulaWeakening: Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
visit(ZOperator) - Method in class owl.ltl.visitors.GeneralFormulaMutator
visit(ZOperator) - Method in class owl.ltl.visitors.PropositionVariablesExtractor
visit(ZOperator) - Method in class owl.ltl.visitors.SolverSyntaxOperatorReplacer
visit(ZOperator) - Method in class owl.ltl.visitors.SubformulaReplacer: Replaces if this node matches SubformulaReplacer.source; otherwise recurses into the operand (past-time "weak yesterday").

W

weakenFormula(Formula, List<String>) - Static method in class geneticalgorithm.SpecificationMutator: Applies the semantically directed weakening mutation, producing a formula φ_w such that φ ⊨ φ_w: every model of the original sub-formula survives (e.g.
WellSeparationAnalysis - Class in main
WellSeparationAnalysis() - Constructor for class main.WellSeparationAnalysis
WON_MODELS_FACTOR - Static variable in class main.Settings: Weight of the won-models direction of the semantic-similarity component (the other half of γ; default 0.1).

A B C D E F G H I L M N O P R S T U V W
All Classes All Packages