Package owl.ltl.visitors

Class SubformulaReplacer

  • All Implemented Interfaces:
    Function<owl.ltl.Formula,​owl.ltl.Formula>, owl.ltl.visitors.Visitor<owl.ltl.Formula>
    public class SubformulaReplacer
extends Object
implements owl.ltl.visitors.Visitor<owl.ltl.Formula>
    Replaces every occurrence of a given sub-formula with another, throughout an LTL formula's syntax tree.

    This is the "splice" step used across AuRUS's genetic operators: after SpecificationMutator rewrites a randomly chosen sub-formula to_mutate (via GeneralFormulaMutator, FormulaWeakening or FormulaStrengthening) into mutated, the change is spliced back into the full assumption or guarantee with new SubformulaReplacer(to_mutate, mutated).apply(original). SpecificationCrossover uses it the same way to graft a fragment transplanted from one parent into the other.

    The pattern. Every visit method below follows the same template: if the current node structurally equals source (via Formula.equals(java.lang.Object)), it is replaced wholesale by target; otherwise the visitor recurses into the node's children and rebuilds the same kind of node from the (possibly already-replaced) results. This is a bottom-up tree rebuild, not an in-place mutation — Formulas are immutable, so the entire path from the match up to the root is reconstructed.

    Replace by value, not by position. Matching is structural equality, not object identity or tree position: if source occurs more than once in the formula (e.g. the same sub-formula appearing under two different conjuncts), every occurrence is replaced in the same pass. This is consistent with how callers obtain source — e.g. FormulaUtils.subformulas(Formula) returns a Set<Formula>, deduplicating structurally identical sub-formulas before one is chosen at random — but is worth keeping in mind: this class has no notion of "the occurrence at this specific tree position", only "occurrences equal to this formula".

    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:
    SpecificationMutator, SpecificationCrossover, FormulaUtils

    • Constructor Summary

      Constructors 
      Constructor Description
      SubformulaReplacer​(owl.ltl.Formula source, owl.ltl.Formula target)
      Creates a replacer that will substitute every occurrence of source with target.

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      owl.ltl.Formula apply​(owl.ltl.Formula formula)
      Entry point: applies the replacement throughout the given formula.
      owl.ltl.Formula visit​(owl.ltl.Biconditional biconditional)
      Replaces if this node matches source; otherwise recurses into both operands.
      owl.ltl.Formula visit​(owl.ltl.BooleanConstant booleanConstant)
      Replaces if this node matches source; a boolean constant has no children to recurse into.
      owl.ltl.Formula visit​(owl.ltl.Conjunction conjunction)
      Replaces if this node matches source; otherwise recurses into every conjunct.
      owl.ltl.Formula visit​(owl.ltl.Disjunction disjunction)
      Replaces if this node matches source; otherwise recurses into every disjunct.
      owl.ltl.Formula visit​(owl.ltl.FOperator fOperator)
      Replaces if this node matches source; otherwise recurses into the operand.
      owl.ltl.Formula visit​(owl.ltl.FrequencyG freq)
      Replaces if this node matches source; otherwise recurses into the operand.
      owl.ltl.Formula visit​(owl.ltl.GOperator gOperator)
      Replaces if this node matches source; otherwise recurses into the operand.
      owl.ltl.Formula visit​(owl.ltl.HOperator hOperator)
      Replaces if this node matches source; otherwise recurses into the operand (past-time "historically").
      owl.ltl.Formula visit​(owl.ltl.Literal literal)
      Replaces if this literal matches source; a literal has no children to recurse into.
      owl.ltl.Formula visit​(owl.ltl.MOperator mOperator)
      Replaces if this node matches source; otherwise recurses into both operands ("strong release").
      owl.ltl.Formula visit​(owl.ltl.OOperator oOperator)
      Replaces if this node matches source; otherwise recurses into the operand (past-time "once").
      owl.ltl.Formula visit​(owl.ltl.ROperator rOperator)
      Replaces if this node matches source; otherwise recurses into both operands ("release").
      owl.ltl.Formula visit​(owl.ltl.SOperator sOperator)
      Replaces if this node matches source; otherwise recurses into both operands (past-time "since").
      owl.ltl.Formula visit​(owl.ltl.TOperator tOperator)
      Replaces if this node matches source; otherwise recurses into both operands (past-time "trigger").
      owl.ltl.Formula visit​(owl.ltl.UOperator uOperator)
      Replaces if this node matches source; otherwise recurses into both operands ("until").
      owl.ltl.Formula visit​(owl.ltl.WOperator wOperator)
      Replaces if this node matches source; otherwise recurses into both operands ("weak until").
      owl.ltl.Formula visit​(owl.ltl.XOperator xOperator)
      Replaces if this node matches source; otherwise recurses into the operand ("next").
      owl.ltl.Formula visit​(owl.ltl.YOperator yOperator)
      Replaces if this node matches source; otherwise recurses into the operand (past-time "yesterday").
      owl.ltl.Formula visit​(owl.ltl.ZOperator zOperator)
      Replaces if this node matches source; otherwise recurses into the operand (past-time "weak yesterday").

    • Constructor Detail

      • SubformulaReplacer

        public SubformulaReplacer​(owl.ltl.Formula source,
                          owl.ltl.Formula target)
        Creates a replacer that will substitute every occurrence of source with target.
        Parameters:
        source - the sub-formula to find
        target - the replacement for every match

    • Method Detail

      • apply

        public owl.ltl.Formula apply​(owl.ltl.Formula formula)
        Entry point: applies the replacement throughout the given formula.
        Specified by:
        apply in interface Function<owl.ltl.Formula,​owl.ltl.Formula>
        Specified by:
        apply in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
        Parameters:
        formula - the formula to rewrite
        Returns:
        the formula with every occurrence of source replaced by target

      • visit

        public owl.ltl.Formula visit​(owl.ltl.Biconditional biconditional)
        Replaces if this node matches source; otherwise recurses into both operands.
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.BooleanConstant booleanConstant)
        Replaces if this node matches source; a boolean constant has no children to recurse into.
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.Conjunction conjunction)
        Replaces if this node matches source; otherwise recurses into every conjunct.
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.Disjunction disjunction)
        Replaces if this node matches source; otherwise recurses into every disjunct.
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.FOperator fOperator)
        Replaces if this node matches source; otherwise recurses into the operand.
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.FrequencyG freq)
        Replaces if this node matches source; otherwise recurses into the operand.
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.GOperator gOperator)
        Replaces if this node matches source; otherwise recurses into the operand.
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.HOperator hOperator)
        Replaces if this node matches source; otherwise recurses into the operand (past-time "historically").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.Literal literal)
        Replaces if this literal matches source; a literal has no children to recurse into.
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.MOperator mOperator)
        Replaces if this node matches source; otherwise recurses into both operands ("strong release").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.OOperator oOperator)
        Replaces if this node matches source; otherwise recurses into the operand (past-time "once").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.ROperator rOperator)
        Replaces if this node matches source; otherwise recurses into both operands ("release").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.SOperator sOperator)
        Replaces if this node matches source; otherwise recurses into both operands (past-time "since").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.TOperator tOperator)
        Replaces if this node matches source; otherwise recurses into both operands (past-time "trigger").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.UOperator uOperator)
        Replaces if this node matches source; otherwise recurses into both operands ("until").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.WOperator wOperator)
        Replaces if this node matches source; otherwise recurses into both operands ("weak until").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.XOperator xOperator)
        Replaces if this node matches source; otherwise recurses into the operand ("next").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.YOperator yOperator)
        Replaces if this node matches source; otherwise recurses into the operand (past-time "yesterday").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>

      • visit

        public owl.ltl.Formula visit​(owl.ltl.ZOperator zOperator)
        Replaces if this node matches source; otherwise recurses into the operand (past-time "weak yesterday").
        Specified by:
        visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>