Package geneticalgorithm

Class SpecificationMutator

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

    The operator proceeds in three steps:

    1. Pick a side. With probability GA_GUARANTEES_PREFERENCE_FACTOR% (flag -GPR) a guarantee is mutated; otherwise an assumption. Unrealisability most often originates in the guarantees, so biasing the factor upward focuses the search there; setting it to 100 protects the assumptions entirely (useful when they encode fixed environment constraints).
    2. Pick a target. A conjunct of the chosen side is selected uniformly at random, and inside it a random sub-formula — not necessarily the root — so that surgical changes deep within a complex formula are possible without restructuring its top level.
    3. Pick a mode. One of three rewritings is applied to the selected sub-formula φ, each drawn with equal probability: a general syntactic mutation (undirected exploration), a weakening (producing φw with φ ⊨ φw — no model of φ is lost), or a strengthening (producing φs with φs ⊨ φ — no new model is added). The rewriting rules per operator are implemented by the FormulaWeakening / FormulaStrengthening visitors.

    Deliberate asymmetry. The mapping from the random draw to the mode differs per side: for assumptions the draw 0 yields the general mutation, while for guarantees it yields a strengthening. Strengthening a guarantee tightens (and can thereby untangle) the system's obligations — e.g. strengthening the antecedent of an implication makes it harder to trigger — whereas for assumptions the productive direction is harder to predict a priori, so undirected exploration is preferred and the fitness function is left to judge. This mirrors the design discussion of the mutation operator in the paper and thesis.

    Mutants whose rewritten formula collapses to false are rejected: the unmodified copy of the specification is returned instead (the caller's deduplication then discards it as identical to its parent), since a false assumption makes the specification vacuously realisable and a false guarantee makes it hopeless — neither conveys intent.

    Guarantee removal. When Settings.allowGuaranteeRemoval is set (flags -removeG / -removeGuarantees) and the guarantee side is selected, with probability Settings.GA_REMOVE_GUARANTEE_PROB% the operator drops the chosen guarantee conjunct entirely instead of rewriting a sub-formula, provided more than one guarantee remains. This is the active counterpart to the structural guard in AutomataBasedModelCountingSpecificationFitness, which only stops penalising shorter guarantee sets once the flag is on but never produces them.

    Assumption removal. Symmetrically, when Settings.allowAssumptionRemoval is set (flags -removeA / -removeAssumptions) and the assumption side is selected, with probability Settings.GA_REMOVE_ASSUMPTION_PROB% the operator drops the chosen assumption conjunct entirely, provided more than one assumption remains. Note this weakens the environment and is not a repair direction on its own; the flag exists mainly to control removal that crossover (and mutations collapsing an assumption to true) could otherwise introduce unchecked — with the flag off, the fitness guard now prunes any candidate with fewer assumptions than the original.

    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.mutate(), SpecificationCrossover

    • Method Summary

      All Methods Static Methods Concrete Methods 
      Modifier and Type Method Description
      static owl.ltl.Formula applyGeneralMutation​(owl.ltl.Formula f, List<String> variables)
      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.
      static owl.ltl.tlsf.Tlsf mutate​(owl.ltl.tlsf.Tlsf spec)
      Applies the three-step mutation operator described in the class documentation to the given specification.
      static owl.ltl.Formula strengthenFormula​(owl.ltl.Formula f, List<String> variables)
      Applies the semantically directed strengthening mutation, producing a formula φs such that φs ⊨ φ: no new model is introduced (e.g.
      static owl.ltl.Formula weakenFormula​(owl.ltl.Formula f, List<String> variables)
      Applies the semantically directed weakening mutation, producing a formula φw such that φ ⊨ φw: every model of the original sub-formula survives (e.g.

    • Constructor Detail

      • SpecificationMutator

        public SpecificationMutator()

    • Method Detail

      • mutate

        public static owl.ltl.tlsf.Tlsf mutate​(owl.ltl.tlsf.Tlsf spec)
        Applies the three-step mutation operator described in the class documentation to the given specification.

        Mode mapping per side (draw ∈ {0, 1, 2}, uniform):

           draw   assumptions      guarantees
   0      general          strengthening   (default modes)
   1      weakening        weakening
   2      strengthening    general

        When Settings.only_inputs_in_assumptions is set, mutations on the assumption side draw fresh literals from the input variables only, preventing the search from "repairing" the environment with constraints over outputs it cannot observe.

        Parameters:
        spec - the specification to mutate
        Returns:
        a fresh specification carrying the mutation — or an unmodified copy of the input when the rewriting collapsed to false

      • applyGeneralMutation

        public static owl.ltl.Formula applyGeneralMutation​(owl.ltl.Formula f,
                                                   List<String> variables)
        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. The formula is first put in negation normal form.

        The per-node mutation probability is 1/MR, where MR is derived from Settings.GA_GENE_MUTATION_RATE: with the default rate (0) it evaluates to the formula size n, yielding the 1/|formula| rule of the experimental setup. Implementation note: the derivation uses integer division, so any explicitly set rate in 1..100 collapses MR to 1 — i.e. every node becomes a mutation candidate, subject to the Settings.GA_GENE_NUM_OF_MUTATIONS cap.

        Parameters:
        f - the formula to mutate
        variables - the variable names fresh literals may be drawn from
        Returns:
        the mutated formula

      • weakenFormula

        public static owl.ltl.Formula weakenFormula​(owl.ltl.Formula f,
                                            List<String> variables)
        Applies the semantically directed weakening mutation, producing a formula φw such that φ ⊨ φw: every model of the original sub-formula survives (e.g. p &rarr; p | q, X &phi; &rarr; F &phi;, &phi; U &psi; &rarr; &phi; W &psi;). Weakening an assumption relaxes a constraint on the environment. Same 1/MR probability scheme (and integer-division caveat) as applyGeneralMutation(Formula, List).
        Parameters:
        f - the formula to weaken
        variables - the variable names fresh literals may be drawn from
        Returns:
        the weakened formula

      • strengthenFormula

        public static owl.ltl.Formula strengthenFormula​(owl.ltl.Formula f,
                                                List<String> variables)
        Applies the semantically directed strengthening mutation, producing a formula φs such that φs ⊨ φ: no new model is introduced (e.g. p &rarr; p & q, F &phi; &rarr; &phi;, &phi; W &psi; &rarr; G &phi;). Strengthening a guarantee tightens the system's obligations — the default move on the guarantee side. Same 1/MR probability scheme (and integer-division caveat) as applyGeneralMutation(Formula, List).
        Parameters:
        f - the formula to strengthen
        variables - the variable names fresh literals may be drawn from
        Returns:
        the strengthened formula