Package geneticalgorithm

Class SpecificationCrossover

  • public class SpecificationCrossover
extends Object
    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.

    Each side (assumptions, guarantees) is recombined independently according to a level drawn by the caller (SpecificationChromosome.crossover(geneticalgorithm.SpecificationChromosome)):

    • Level 0 — wholesale swap. The whole side is inherited from one parent chosen by a coin flip. No mixing; the coarsest form of recombination.
    • Level 1 — conjunct merge. The side is built as the union of a random subset of each parent's conjuncts (each conjunct kept with probability ½, duplicates and true skipped — see selectRandomly(List)). Conjuncts travel whole between parents; the offspring may also lose conjuncts both parents had.
    • Level 2 (default branch) — sub-formula merge. The deepest form of mixing: the side starts as parent 0's conjuncts, one random conjunct φ0 is removed, a random conjunct φ1 of parent 1 is picked, and the two are fused at the syntax-tree level — either replaceSubformula (a random sub-tree of φ0 is replaced by φ1) or combineSubformula (they are joined under a random binary connective), with equal probability.

    Bloat control. A level-2 merged conjunct is accepted only if it contains at most two temporal operators; this guards the search against the classic genetic-programming pathology of ever-growing formulas. Note the side effect: when the merge fails the guard, the removed conjunct φ0 is not restored, so level-2 crossover can shrink a specification by one conjunct.

    Restrictions. The guarantee-preference factor gates which sides may mix at levels 1–2 (assumptions only when -GPR < 100, guarantees only when -GPR > 0; a frozen side is copied verbatim from parent 0). When -onlyInputsA is set, the fragment transplanted into an assumption is first restricted to a sub-formula over input variables only (falling back to true if none exists), preventing the environment from being "repaired" with constraints over outputs.

    The operator makes no consistency promise: offspring may well be unsatisfiable or unrealisable. Judging them is deliberately left to the fitness function, whose graded status ladder rewards partially consistent candidates.

    Part of the reference implementation of: Brizzio, Cordy, Papadakis, Sánchez, Aguirre, Degiovanni. "Automated Repair of Unrealisable LTL Specifications Guided by Model Counting", GECCO 2023 (doi:10.1145/3583131.3590454).

    Author:
    Matías Brizzio
    See Also:
    SpecificationChromosome, SpecificationMutator

    • Constructor Detail

      • SpecificationCrossover

        public SpecificationCrossover()

    • Method Detail

      • apply

        public static List<owl.ltl.tlsf.Tlsf> apply​(owl.ltl.tlsf.Tlsf spec0,
                                            owl.ltl.tlsf.Tlsf spec1,
                                            int assumption_level,
                                            int guarantee_level)
        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).

        The offspring inherits everything else (inputs, outputs, initial conditions, ...) from spec0. At most one offspring is produced; the list is empty when the resulting guarantee side would be empty.

        Parameters:
        spec0 - the first parent (also the template for the offspring)
        spec1 - the second parent
        assumption_level - recombination level for the assumption side
        guarantee_level - recombination level for the guarantee side
        Returns:
        a singleton list with the offspring, or an empty list