```
public class Settings
extends Object
```
Central, static configuration of AuRUS: every knob the genetic search, the fitness function, the model counter and the external solvers read from.
Fields are grouped by concern below, each documented with the command-line flag that sets it (see Main), its default, and — where useful — a pointer to the class that reads it. This mirrors the "Configuration reference" tables in the project README; the two should be read together.

All fields are public static and mutable by design: Main parses the command line once at start-up and writes directly into this class, and every other class reads from it for the rest of the run. There is deliberately no per-run instance — AuRUS runs one search per process.

Author:

Matías Brizzio

See Also:

Main, SpecificationGeneticAlgorithm, AutomataBasedModelCountingSpecificationFitness

Field Summary

Fields
Modifier and Type	Field	Description
`static boolean`	`allowAssumptionAddition`	Allow the genetic operators to introduce brand-new assumptions rather than only modifying existing ones (flags `-addA`/`-addAssumptions`, default `false`).
`static boolean`	`allowAssumptionRemoval`	Allow the genetic operators to drop assumptions entirely (flags `-removeA`/`-removeAssumptions`, default `false`).
`static boolean`	`allowGuaranteeRemoval`	Allow the genetic operators to drop guarantees entirely (flags `-removeG`/`-removeGuarantees`, default `false`).
`static boolean`	`check_REALIZABILITY`	Whether realisability (via Strix, or strong satisfiability when `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`).
`static boolean`	`check_STRONG_SAT`	Use the strong-satisfiability (potential realisability) check instead of a full Strix realisability query inside the fitness (flag `-strongSAT`, default `false`) — cheaper, less precise.
`static int`	`GA_CROSSOVER_RATE`	Percentage of chromosomes selected for crossover at each generation (flag `-COR`, default `10`).
`static int`	`GA_EXECUTION_TIMEOUT`	Overall wall-clock budget for the genetic search, in seconds (flag `-GATO`, default `0` — no timeout).
`static int`	`GA_GENE_MUTATION_RATE`	Probability (%) with which each gene (sub-formula) of a mutated chromosome is itself mutated (flag `-geneMR`, default `0`).
`static int`	`GA_GENE_NUM_OF_MUTATIONS`	Maximum number of genes (sub-formulas) mutated per formula (flag `-geneNUM`, default `0`).
`static int`	`GA_GENERATIONS`	Number of generations the search runs for (flag `-Gen`, default `10`).
`static int`	`GA_GUARANTEES_PREFERENCE_FACTOR`	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`).
`static int`	`GA_MAX_NUM_INDIVIDUALS`	Hard cap on the total number of individuals ever generated, across all generations (flag `-Max`, default: unbounded).
`static int`	`GA_MUTATION_RATE`	Probability (%) with which the mutation operator is applied to each chromosome (flag `-MR`, default `100` — always).
`static int`	`GA_POPULATION_SIZE`	Population size retained at each generation (flag `-Pop`, default `100`).
`static boolean`	`GA_RANDOM_SELECTOR`	Use a random selector instead of the best-selector for the next generation's parents (flag `-GA_random_selector`, default `false`).
`static int`	`GA_REMOVE_ASSUMPTION_PROB`	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`).
`static int`	`GA_REMOVE_GUARANTEE_PROB`	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`).
`static double`	`GA_THRESHOLD`	Minimum fitness a candidate must reach to be collected as a solution during the search (flag `-sol`, default `0.0` — no threshold).
`static double`	`LOST_MODELS_FACTOR`	Weight of the lost-models direction of the semantic-similarity component (half of γ from `-factors`; default `0.1`).
`static int`	`MC_BOUND`	Bound `k` for the bounded model-counting approach (flag `-k`, default `10`).
`static boolean`	`MC_EXHAUSTIVE`	Intended to select an exact model counter instead of the automata/matrix approximation (flag `-precise` sets this to `false`; default `true`).
`static int`	`MC_TIMEOUT`	Timeout, in seconds, for a single bounded model-counting query (flag `-MCTO`, default `180`).
`static boolean`	`only_inputs_in_assumptions`	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.
`static int`	`PARSING_TIMEOUT`	Timeout, in seconds, for translating a formula into its automaton (default `60`).
`static Random`	`RANDOM_GENERATOR`	Shared random source for every stochastic decision in the search (selection coin flips, mutation targets, ...), seeded from `SEED`.
`static int`	`SAT_TIMEOUT`	Timeout, in seconds, for a single LTL satisfiability query (flag `-SatTO`, default `30`).
`static long`	`SEED`	The seed backing `RANDOM_GENERATOR`.
`static String`	`SPECTRA_PATH`	Working directory used when checking realisability of Spectra specifications (`-use-spectra`, default `"docker-spectra/"`).
`static double`	`STATUS_FACTOR`	Weight α of the realisability-status component in the fitness sum (flag `-factors`, first value; default `0.7`).
`static String`	`STRIX_PATH`	Working directory Strix (native or Docker) reads/writes its temporary TLSF files in; overridden to the output directory via `setStrixName(java.lang.String)` when `-out` is given (default `"docker/"`).
`static int`	`STRIX_TIMEOUT`	Timeout, in seconds, for a single Strix realisability query (flag `-RTO`, default `20`).
`static int`	`STRONG_SAT_TIMEOUT`	Timeout, in seconds, for a strong-satisfiability query (default `180`).
`static double`	`SYNTACTIC_FACTOR`	Weight β of the syntactic-similarity component in the fitness sum (flag `-factors`, second value; default `0.1`).
`static String`	`SYNTH_BIN`	Path/name of the synthesiser binary to invoke for `SYNTH_TOOL` (flag `-synth-bin`).
`static String`	`SYNTH_TOOL`	Which realisability/synthesis tool to invoke (flag `-synth`, default `"strix"`).
`static boolean`	`USE_DOCKER`	Run Strix through the Docker image rather than the local install (flags `-docker`/`-no-docker`, default `false` — native).
`static boolean`	`USE_SPECTRA`	Treat the input as a Spectra specification instead of TLSF (flag `-use-spectra`, default `false`).
`static double`	`WON_MODELS_FACTOR`	Weight of the won-models direction of the semantic-similarity component (the other half of γ; default `0.1`).

Constructor Summary

Constructors
Constructor Description

Settings()

Method Summary

All Methods Static Methods Concrete Methods
Modifier and Type	Method	Description
`static double`	`MAX_FITNESS()`	Theoretical maximum value the fitness function can return: the sum of all four component weights.
`static String`	`print_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`.
`static void`	`setFactors(double status_factor, double syntactic_factor, double semantic_factor)`	Sets the three top-level fitness weights (realisability status, syntactic similarity, semantic similarity), splitting the semantic weight evenly between `LOST_MODELS_FACTOR` and `WON_MODELS_FACTOR`.
`static void`	`setStrixName(String outname)`	Redirects `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.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - USE_SPECTRA
```
public static boolean USE_SPECTRA
```
    Treat the input as a Spectra specification instead of TLSF (flag -use-spectra, default false).
  - USE_DOCKER
```
public static boolean USE_DOCKER
```
    Run Strix through the Docker image rather than the local install (flags -docker/-no-docker, default false — native). By default (no Docker, no Spectra), AuRUS calls lib/new_strix/strix directly; see StrixHelper for the exact dispatch.
  - SYNTH_TOOL
```
public static String SYNTH_TOOL
```
    Which realisability/synthesis tool to invoke (flag -synth, default "strix"). Currently supported: "strix" (the original path — native binary, or the Docker image when USE_DOCKER is set) and "ltlsynt" (part of the Spot library, installable without Docker via e.g. brew install spot (macOS) or conda install -c conda-forge spot (Linux/macOS, no root needed) — see spot.lre.epita.fr/install.html for the Debian/Ubuntu package repository. Read by StrixHelper.
  - SYNTH_BIN
```
public static String SYNTH_BIN
```
    Path/name of the synthesiser binary to invoke for SYNTH_TOOL (flag -synth-bin). Empty means "use the tool's default": lib/new_strix/strix for strix, or ltlsynt resolved from PATH for ltlsynt.
  - SEED
```
public static long SEED
```
    The seed backing RANDOM_GENERATOR. Auto-generated by default (so runs are non-deterministic out of the box) from the system clock, mixed with the 64-bit golden-ratio constant (0x9E3779B97F4A7C15) for good bit dispersion (the standard Fibonacci/golden-ratio hashing trick — avoids the low bits of consecutive System.nanoTime() calls correlating between close-together runs). Always a concrete value — printed by print_settings() in every out.txt — so any past run can be reproduced after the fact by passing -seed=<that value>, even if it wasn't explicitly seeded when it originally ran. Explicitly setting it (flag -seed) makes AuRUS's own stochastic decisions (selection, mutation targets, crossover choices) reproducible given the same sequence of external solver verdicts — see the project TODO.md for the current, honest state of end-to-end reproducibility (not yet complete: at least one additional source of run-to-run variance remains, independent of this seed).
  - RANDOM_GENERATOR
```
public static Random RANDOM_GENERATOR
```
    Shared random source for every stochastic decision in the search (selection coin flips, mutation targets, ...), seeded from SEED. Reproducible across runs when SEED is set explicitly via -seed.
  - GA_GENERATIONS
```
public static int GA_GENERATIONS
```
    Number of generations the search runs for (flag -Gen, default 10). Read by SpecificationGeneticAlgorithm.
  - GA_MAX_NUM_INDIVIDUALS
```
public static int GA_MAX_NUM_INDIVIDUALS
```
    Hard cap on the total number of individuals ever generated, across all generations (flag -Max, default: unbounded).
  - GA_POPULATION_SIZE
```
public static int GA_POPULATION_SIZE
```
    Population size retained at each generation (flag -Pop, default 100).
  - GA_CROSSOVER_RATE
```
public static int GA_CROSSOVER_RATE
```
    Percentage of chromosomes selected for crossover at each generation (flag -COR, default 10).
  - GA_MUTATION_RATE
```
public static int GA_MUTATION_RATE
```
    Probability (%) with which the mutation operator is applied to each chromosome (flag -MR, default 100 — always).
  - GA_GENE_MUTATION_RATE
```
public static int GA_GENE_MUTATION_RATE
```
    Probability (%) with which each gene (sub-formula) of a mutated chromosome is itself mutated (flag -geneMR, default 0). A value of 0 means the rate is derived as 1/size_of(formula) — the rule used in the paper's experimental setup — rather than a fixed percentage; see SpecificationMutator.
  - GA_GENE_NUM_OF_MUTATIONS
```
public static int GA_GENE_NUM_OF_MUTATIONS
```
    Maximum number of genes (sub-formulas) mutated per formula (flag -geneNUM, default 0). A value of 0 means no cap — up to size_of(formula) mutations may be applied.
  - GA_EXECUTION_TIMEOUT
```
public static int GA_EXECUTION_TIMEOUT
```
    Overall wall-clock budget for the genetic search, in seconds (flag -GATO, default 0 — no timeout).
  - GA_GUARANTEES_PREFERENCE_FACTOR
```
public static int GA_GUARANTEES_PREFERENCE_FACTOR
```
    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). p = 0 protects the guarantees entirely, p = 100 protects the assumptions — useful when one side encodes fixed, non-negotiable constraints.
  - GA_RANDOM_SELECTOR
```
public static boolean GA_RANDOM_SELECTOR
```
    Use a random selector instead of the best-selector for the next generation's parents (flag -GA_random_selector, default false). Read by com.lagodiuk.ga.GeneticAlgorithm, the underlying GA engine.
  - only_inputs_in_assumptions
```
public static boolean only_inputs_in_assumptions
```
    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.
  - GA_THRESHOLD
```
public static double GA_THRESHOLD
```
    Minimum fitness a candidate must reach to be collected as a solution during the search (flag -sol, default 0.0 — no threshold).
  - check_REALIZABILITY
```
public static boolean check_REALIZABILITY
```
    Whether realisability (via Strix, or strong satisfiability when 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). See AutomataBasedModelCountingSpecificationFitness.compute_status(geneticalgorithm.SpecificationChromosome).
  - check_STRONG_SAT
```
public static boolean check_STRONG_SAT
```
    Use the strong-satisfiability (potential realisability) check instead of a full Strix realisability query inside the fitness (flag -strongSAT, default false) — cheaper, less precise.
  - allowAssumptionAddition
```
public static boolean allowAssumptionAddition
```
    Allow the genetic operators to introduce brand-new assumptions rather than only modifying existing ones (flags -addA/-addAssumptions, default false).
  - allowGuaranteeRemoval
```
public static boolean allowGuaranteeRemoval
```
    Allow the genetic operators to drop guarantees entirely (flags -removeG/-removeGuarantees, default false).
  - allowAssumptionRemoval
```
public static boolean allowAssumptionRemoval
```
    Allow the genetic operators to drop assumptions entirely (flags -removeA/-removeAssumptions, default false).
  - GA_REMOVE_ASSUMPTION_PROB
```
public static int GA_REMOVE_ASSUMPTION_PROB
```
    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
```
public static int GA_REMOVE_GUARANTEE_PROB
```
    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).
  - STATUS_FACTOR
```
public static double STATUS_FACTOR
```
    Weight α of the realisability-status component in the fitness sum (flag -factors, first value; default 0.7). Set together with the other three factors via setFactors(double, double, double).
  - LOST_MODELS_FACTOR
```
public static double LOST_MODELS_FACTOR
```
    Weight of the lost-models direction of the semantic-similarity component (half of γ from -factors; default 0.1). See docs/FITNESS.md.
  - WON_MODELS_FACTOR
```
public static double WON_MODELS_FACTOR
```
    Weight of the won-models direction of the semantic-similarity component (the other half of γ; default 0.1). See docs/FITNESS.md.
  - SYNTACTIC_FACTOR
```
public static double SYNTACTIC_FACTOR
```
    Weight β of the syntactic-similarity component in the fitness sum (flag -factors, second value; default 0.1).
  - PARSING_TIMEOUT
```
public static int PARSING_TIMEOUT
```
    Timeout, in seconds, for translating a formula into its automaton (default 60). Read by EmersonLeiAutomatonBasedModelCounting.
  - MC_BOUND
```
public static int MC_BOUND
```
    Bound k for the bounded model-counting approach (flag -k, default 10). See docs/FITNESS.md for what the bound controls.
  - MC_EXHAUSTIVE
```
public static boolean MC_EXHAUSTIVE
```
    Intended to select an exact model counter instead of the automata/matrix approximation (flag -precise sets this to false; default true). Currently unused: no counting code path reads this field, so -precise has no effect on the search — see the project TODO.md.
  - MC_TIMEOUT
```
public static int MC_TIMEOUT
```
    Timeout, in seconds, for a single bounded model-counting query (flag -MCTO, default 180).
  - STRIX_TIMEOUT
```
public static int STRIX_TIMEOUT
```
    Timeout, in seconds, for a single Strix realisability query (flag -RTO, default 20).
  - STRIX_PATH
```
public static String STRIX_PATH
```
    Working directory Strix (native or Docker) reads/writes its temporary TLSF files in; overridden to the output directory via setStrixName(java.lang.String) when -out is given (default "docker/"). Read by TlsfUtils.
  - SPECTRA_PATH
```
public static String SPECTRA_PATH
```
    Working directory used when checking realisability of Spectra specifications (-use-spectra, default "docker-spectra/"). Read by StrixHelper.
  - STRONG_SAT_TIMEOUT
```
public static int STRONG_SAT_TIMEOUT
```
    Timeout, in seconds, for a strong-satisfiability query (default 180).
  - SAT_TIMEOUT
```
public static int SAT_TIMEOUT
```
    Timeout, in seconds, for a single LTL satisfiability query (flag -SatTO, default 30).
- Constructor Detail
  - Settings
```
public Settings()
```
- Method Detail
  - MAX_FITNESS
```
public static double MAX_FITNESS()
```
    Theoretical maximum value the fitness function can return: the sum of all four component weights. Used as a sanity ceiling — a computed fitness above this value indicates a configuration or arithmetic bug (see AutomataBasedModelCountingSpecificationFitness.calculate(geneticalgorithm.SpecificationChromosome)).
    
    Returns:
    
    STATUS_FACTOR + LOST_MODELS_FACTOR + WON_MODELS_FACTOR + SYNTACTIC_FACTOR
  - setFactors
```
public static void setFactors(double status_factor,
                              double syntactic_factor,
                              double semantic_factor)
```
    Sets the three top-level fitness weights (realisability status, syntactic similarity, semantic similarity), splitting the semantic weight evenly between LOST_MODELS_FACTOR and WON_MODELS_FACTOR. A negative argument leaves the corresponding setting(s) untouched, so callers can update a subset of the weights (this is how -factors is applied, and how SpecificationGeneticAlgorithm.run(owl.ltl.tlsf.Tlsf) — which passes all three as -1.0 — keeps the currently configured weights).
    
    Parameters:
    
    status_factor - new value for STATUS_FACTOR, or negative to keep the current one
    
    syntactic_factor - new value for SYNTACTIC_FACTOR, or negative to keep the current one
    
    semantic_factor - new combined weight to split across LOST_MODELS_FACTOR and WON_MODELS_FACTOR, or negative to keep the current ones
  - setStrixName
```
public static void setStrixName(String outname)
```
    Redirects 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.
    
    Parameters:
    
    outname - the output directory (as passed to -out)
  - print_settings
```
public static String print_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.
    
    Returns:
    
    a human-readable, single-line summary of the current configuration

Class Settings

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

USE_SPECTRA

USE_DOCKER

SYNTH_TOOL

SYNTH_BIN

SEED

RANDOM_GENERATOR

GA_GENERATIONS

GA_MAX_NUM_INDIVIDUALS

GA_POPULATION_SIZE

GA_CROSSOVER_RATE

GA_MUTATION_RATE

GA_GENE_MUTATION_RATE

GA_GENE_NUM_OF_MUTATIONS

GA_EXECUTION_TIMEOUT

GA_GUARANTEES_PREFERENCE_FACTOR

GA_RANDOM_SELECTOR

only_inputs_in_assumptions

GA_THRESHOLD

check_REALIZABILITY

check_STRONG_SAT

allowAssumptionAddition

allowGuaranteeRemoval

allowAssumptionRemoval

GA_REMOVE_ASSUMPTION_PROB

GA_REMOVE_GUARANTEE_PROB

STATUS_FACTOR

LOST_MODELS_FACTOR

WON_MODELS_FACTOR

SYNTACTIC_FACTOR

PARSING_TIMEOUT

MC_BOUND

MC_EXHAUSTIVE

MC_TIMEOUT

STRIX_TIMEOUT

STRIX_PATH

SPECTRA_PATH

STRONG_SAT_TIMEOUT

SAT_TIMEOUT

Constructor Detail

Settings

Method Detail

MAX_FITNESS

setFactors

setStrixName

print_settings