java.lang.Object
- owl.ltl.visitors.FormulaWeakening

All Implemented Interfaces:

Function<owl.ltl.Formula,owl.ltl.Formula>, owl.ltl.visitors.Visitor<owl.ltl.Formula>
```
public class FormulaWeakening
extends Object
implements owl.ltl.visitors.Visitor<owl.ltl.Formula>
```
The weakening mutation mode of AuRUS: rewrites an LTL formula (in negation normal form) into a semantically weaker one, i.e. a formula φ_w such that φ ⊨ φ_w — every model of the original formula survives the rewrite. Applied to an assumption, this relaxes a constraint on the environment; see FormulaStrengthening for the dual mode, and geneticalgorithm.SpecificationMutator for how the two are selected during the search.
This class implements the weakening rules of Table 4.1 in the paper and thesis this project is the reference implementation of (one visit method per LTL operator, one rewrite rule per numbered option); see the individual visit methods below for the correspondence. The two additional operators M (strong release) and R (release) are handled via their standard dualities with U/W (noted inline) rather than appearing as separate rows in the thesis table.

How mutation is applied. This is a recursive Visitor: it walks the formula bottom-up, and at every node — not just the root — it may independently roll the dice to weaken that node. Two knobs control this, both threaded through the constructor:
- weakening_rate — the per-node mutation probability is 1/weakening_rate (a fresh Random.nextInt(weakening_rate) == 0 roll at each node); see SpecificationMutator.weakenFormula, which derives this from Settings.GA_GENE_MUTATION_RATE.
- numOfAllowedWeakening — a mutable budget, decremented every time a node is actually weakened; once it reaches 0, no further node is touched, bounding how many changes one mutation call can make to a single formula.
Bloat guard. Several visit methods count the number of temporal operators in the (already partially rewritten) current formula and abandon further weakening of that node — returning the original, unweakened sub-formula — once the count exceeds 2. This keeps mutated formulas from growing without bound, the classic bloat problem in genetic-programming-style search.

Universal weakest bound. At every node, one of the random options is simply true — the weakest possible formula — giving the search a way to discard a sub-formula entirely regardless of its shape.

A note on soundness of the fallback rules. Most rules below are the same directed rewrites as the thesis table and are sound by construction (entailment-preserving for every substitution of the variables involved). A few fallback branches — e.g. the last option of visit(FOperator), visit(UOperator) and visit(WOperator), which combine the current formula with a freshly drawn, but not fresh in the logical sense, existing proposition via new_literal(Formula) — are not guaranteed entailments for every possible choice of that proposition (e.g. F(a) ⊨ c W a does not hold for every c). These branches are best understood as heuristic exploration in the spirit of the undirected general mutation, injected into the weakening operator for extra diversity; any resulting semantic drift is caught downstream by the fitness function's semantic-similarity component, not by this class.

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:

FormulaStrengthening, GeneralFormulaMutator

Constructor Summary

Constructors
Constructor	Description
`FormulaWeakening(List<String> literals, int weakening_rate, int num_of_weakening_to_apply)`	Creates a weakening visitor over the given variable alphabet.

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`owl.ltl.Formula`	`apply(owl.ltl.Formula formula)`	Entry point: applies this visitor to the root of the given formula.
`owl.ltl.Literal`	`new_literal(owl.ltl.Formula current)`	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.
`List<String>`	`variables()`
`owl.ltl.Formula`	`visit(owl.ltl.Biconditional biconditional)`	Rejected: the mutator only ever runs on formulas already converted to negation normal form.
`owl.ltl.Formula`	`visit(owl.ltl.BooleanConstant booleanConstant)`	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).
`owl.ltl.Formula`	`visit(owl.ltl.Conjunction conjunction)`	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).
`owl.ltl.Formula`	`visit(owl.ltl.Disjunction disjunction)`	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).
`owl.ltl.Formula`	`visit(owl.ltl.FOperator fOperator)`	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.
`owl.ltl.Formula`	`visit(owl.ltl.FrequencyG freq)`	Rejected: the mutator only ever runs on formulas already converted to negation normal form.
`owl.ltl.Formula`	`visit(owl.ltl.GOperator gOperator)`	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).
`owl.ltl.Formula`	`visit(owl.ltl.HOperator hOperator)`	Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
`owl.ltl.Formula`	`visit(owl.ltl.Literal literal)`	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").
`owl.ltl.Formula`	`visit(owl.ltl.MOperator mOperator)`	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).
`owl.ltl.Formula`	`visit(owl.ltl.OOperator oOperator)`	Rejected: the mutator only ever runs on formulas already converted to negation normal form.
`owl.ltl.Formula`	`visit(owl.ltl.ROperator rOperator)`	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).
`owl.ltl.Formula`	`visit(owl.ltl.SOperator sOperator)`	Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
`owl.ltl.Formula`	`visit(owl.ltl.TOperator tOperator)`	Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
`owl.ltl.Formula`	`visit(owl.ltl.UOperator uOperator)`	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`).
`owl.ltl.Formula`	`visit(owl.ltl.WOperator wOperator)`	Weakens `a W b` ("`a` holds unless/until `b`", recursing into both sides first).
`owl.ltl.Formula`	`visit(owl.ltl.XOperator xOperator)`	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).
`owl.ltl.Formula`	`visit(owl.ltl.YOperator yOperator)`	Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
`owl.ltl.Formula`	`visit(owl.ltl.ZOperator zOperator)`	Rejected: past-time operator, not expected in the LTL fragment this mutator handles.

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

Methods inherited from interface java.util.function.Function
andThen, compose

- Constructor Detail
  - FormulaWeakening
```
public FormulaWeakening(List<String> literals,
                        int weakening_rate,
                        int num_of_weakening_to_apply)
```
    Creates a weakening visitor over the given variable alphabet.
    
    Parameters:
    
    literals - the specification's variable names, in index order
    
    weakening_rate - per-node mutation probability is 1/weakening_rate
    
    num_of_weakening_to_apply - maximum number of sub-formulas this visitor may weaken in one pass
- Method Detail
  - variables
```
public List<String> variables()
```
    Returns:
    
    a defensive copy of the variable alphabet this visitor was built with
  - apply
```
public owl.ltl.Formula apply(owl.ltl.Formula formula)
```
    Entry point: applies this visitor to the root of 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 weaken (should be in negation normal form)
    
    Returns:
    
    the (possibly) weakened formula
  - visit
```
public owl.ltl.Formula visit(owl.ltl.BooleanConstant booleanConstant)
```
    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).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.Literal literal)
```
    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").
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.XOperator xOperator)
```
    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).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.FOperator fOperator)
```
    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.
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.GOperator gOperator)
```
    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).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.Conjunction conjunction)
```
    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).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.Disjunction disjunction)
```
    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).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.UOperator uOperator)
```
    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).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.WOperator wOperator)
```
    Weakens a W b ("a holds unless/until b", recursing into both sides first). Recalling that a W b ≡ G(a) ∨ (a U b), this weakens one of the two disjuncts at a time: true (option 0); F(a) ∨ (a U b) (option 1 — relaxing the "always" disjunct down to "eventually"); G(a) ∨ F(b) (option 2 — relaxing the "until" disjunct down to a bare "eventually"); or (a ∨ c) W b for a drawn literal c (option 3 — widening what may hold throughout).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.MOperator mOperator)
```
    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).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.ROperator rOperator)
```
    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).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.Biconditional biconditional)
```
    Rejected: the mutator only ever runs on formulas already converted to negation normal form.
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.FrequencyG freq)
```
    Rejected: the mutator only ever runs on formulas already converted to negation normal form.
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.OOperator oOperator)
```
    Rejected: the mutator only ever runs on formulas already converted to negation normal form.
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.HOperator hOperator)
```
    Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.TOperator tOperator)
```
    Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.SOperator sOperator)
```
    Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.YOperator yOperator)
```
    Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.ZOperator zOperator)
```
    Rejected: past-time operator, not expected in the LTL fragment this mutator handles.
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - new_literal
```
public owl.ltl.Literal new_literal(owl.ltl.Formula current)
```
    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. Tries (up to 5 attempts) to avoid a variable already appearing (positively or negatively) in current, then negates the result with 50% probability. Note this is not a logically fresh Skolem variable: it is drawn from the same fixed, finite alphabet as every other proposition in the specification, which is what underlies the soundness caveat discussed in the class documentation.
    
    Parameters:
    
    current - the formula being weakened, used only to bias the draw away from its own propositions
    
    Returns:
    
    a literal (possibly negated) from the variable alphabet

Class FormulaWeakening

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Methods inherited from interface java.util.function.Function

Constructor Detail

FormulaWeakening

Method Detail

variables

apply

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

visit

new_literal