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

All Implemented Interfaces:

Function<owl.ltl.Formula,owl.ltl.Formula>, owl.ltl.visitors.Visitor<owl.ltl.Formula>
```
public class FormulaStrengthening
extends Object
implements owl.ltl.visitors.Visitor<owl.ltl.Formula>
```
The strengthening mutation mode of AuRUS: rewrites an LTL formula (in negation normal form) into a semantically stronger one, i.e. a formula φ_s such that φ_s ⊨ φ — no new model is introduced by the rewrite. Applied to a guarantee, this tightens an obligation on the system — the default direction for guarantee mutations, since unrealisability most often originates there (see geneticalgorithm.SpecificationMutator). See FormulaWeakening for the dual mode; the two classes are structural mirrors of each other, operator for operator.
This class implements the strengthening 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 strengthen that node. Two knobs control this, both threaded through the constructor, mirroring FormulaWeakening: strengthening_rate (per-node mutation probability 1/strengthening_rate) and numOfAllowedStrengthenings (a mutable budget of remaining mutations, decremented on each applied change).

Bloat guard. As in FormulaWeakening, several visit methods count the number of temporal operators in the (already partially rewritten) current formula and abandon further strengthening of that node — returning the original sub-formula — once the count exceeds 2.

Universal strongest bound. At every node, one of the random options is simply false — the strongest possible formula — giving the search a way to discard a sub-formula's satisfiability entirely.

A note on soundness of the fallback rules. As with FormulaWeakening, most rules below are sound by construction. The unrolling fallback branches of visit(UOperator), visit(FOperator) (option 7) and their siblings, which introduce a fresh draw via new_literal(Formula), share the same caveat documented there: the drawn proposition is taken from the same fixed alphabet as the rest of the specification, not a logically fresh variable, so these particular branches are heuristic exploration rather than guaranteed entailments for every possible draw.

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:

FormulaWeakening, GeneralFormulaMutator

Constructor Summary

Constructors
Constructor	Description
`FormulaStrengthening(List<String> literals, int strengthening_rate, int num_of_strengthening_to_apply)`	Creates a strengthening 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 strengthened.
`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)`	Strengthens a boolean constant: `true ⤳ false` (the only possible strengthening of a constant; `false` is already the strongest formula and is left untouched by the random draw).
`owl.ltl.Formula`	`visit(owl.ltl.Conjunction conjunction)`	Strengthens a conjunction `a1 ∧ ... ∧ an` (recursing into every conjunct first) into one of: `false` (option 0); adding one more conjunct drawn from the alphabet, `a1 ∧ a2 ⤳ a1 ∧ a2 ∧ c` (option 1 — a conjunction can only become more demanding by adding conjuncts); or, when not already temporally heavy, `G(a1 ∧ ... ∧ an)` (option 2 — requiring the whole conjunction to hold forever rather than just now).
`owl.ltl.Formula`	`visit(owl.ltl.Disjunction disjunction)`	Strengthens a disjunction `a1 ∨ ... ∨ an` (recursing into every disjunct first) into one of: `false` (option 0); turning the whole disjunction into a conjunction, `a1 ∨ a2 ⤳ a1 ∧ a2` (option 1 — Table 4.1's "conjunct" rule); dropping one randomly chosen disjunct, `a1 ∨ a2 ⤳ a1` (option 2 — narrowing which alternative is allowed); or, when not already temporally heavy, `G(a1 ∨ ... ∨ an)` (option 3 — requiring the disjunction to hold forever rather than just now).
`owl.ltl.Formula`	`visit(owl.ltl.FOperator fOperator)`	Strengthens `F(a)` (recursing into `a` first) into one of, drawn uniformly out of 8 outcomes: `false` (option 0); `a` itself (option 1 — requiring it now rather than eventually); `X(a)` (option 2 — requiring it at the very next step); `G(a)` (option 3 — requiring it forever, Table 4.1's strongest "eventually" tightening); `F X(a)` (option 4, guarded against runaway size — delaying by exactly one step); `F G(a)` (option 5, same guard — "eventually always", strictly implying plain "eventually"); `G F(a)` (option 6, same guard — "infinitely often" is the valid strengthening direction of "eventually always", the mirror of `FormulaWeakening.visit(GOperator)`'s weakening of `G F` down to `F G`); or `a U b` for a drawn literal `b` (option 7 — requiring `a` to hold at least until some point, rather than merely eventually).
`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)`	Strengthens `G(a)` (recursing into `a` first) into one of, drawn uniformly out of 5 outcomes: `false` (option 0, default); distributing over a disjunction, `G(a1 ∨ a2) ⤳ G(a1) ∨ G(a2)` (option 1, only when `a` is a disjunction, via the disjunctive normal form of the operand — each disjunct is required to hold forever on its own, rather than the weaker requirement that some disjunct hold at each step); `G F(b) ⤳ F G(b)` (option 2, when `a = F(b)` — the valid strengthening direction noted above); simplifying `G X(b)` down to `G(b)` (option 3, when `a = X(b)` — equivalent, since "always" already covers the next step); or simplifying the (already-idempotent) `G G(b)` down to `G(b)` (option 4, when `a` is itself a `G`-formula — a non-strict, equivalence-preserving simplification rather than a proper strengthening).
`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)`	Strengthens an atomic literal `p` into one of, chosen uniformly at random: `false` (option 0); `p ∧ q` for a fresh literal `q` (option 1 — Table 4.1's "add conjunct" rule); or `G(p)` (option 2 — "always" is stronger than "now").
`owl.ltl.Formula`	`visit(owl.ltl.MOperator mOperator)`	Strengthens `a M b` ("strong release" — via the standard duality `a M b ≡ b U (a ∧ b)`, and its own unrolling `≡ (a ∧ b) ∨ (b ∧ ¬(a ∧ b) ∧ X(b U (a ∧ b)))` — recursing into both sides first) into one of: `false` (option 0); `a ∧ b` (option 1 — requiring the joint condition to hold now, the strongest immediate reading); or `b ∧ ¬(a ∧ b) ∧ X(a M b)` (option 2 — unrolling one step of the "strong release" 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)`	Strengthens `a R b` ("release" — via the standard duality `a R b ≡ b W (a ∧ b) ≡ G(b) ∨ (a M b)` — recursing into both sides first) into one of: `false` (option 0); `G(b)` (option 1 — keeping only the "always `b`" disjunct); or `a M b` (option 2 — keeping only the "strong release" disjunct, strictly stronger than the original release).
`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)`	Strengthens `a U b` (recursing into both sides first) via its unrolling `a U b ≡ b ∨ (a ∧ ¬b ∧ X(a U b))`, into one of: `false` (option 0); `b` (option 1 — requiring the eventual condition to hold now, dropping the "until" build-up entirely); or, when not already temporally heavy, `a ∧ ¬b ∧ X(a U b)` (option 2 — unrolling one step: `a` must hold now, `b` must not yet, and the same obligation continues from the next step).
`owl.ltl.Formula`	`visit(owl.ltl.WOperator wOperator)`	Strengthens `a W b` (recursing into both sides first).
`owl.ltl.Formula`	`visit(owl.ltl.XOperator xOperator)`	Strengthens `X(a)` (recursing into `a` first) into one of: `false` (option 0, default); `G(a)` (option 1 — "always" from the next step on is stronger than a single "next"); or, when `a` is itself `G(b)`, simplifying `X G(b)` down to `G(b)` (option 2 — equivalent, since "always from the next step" already implies "always").
`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
  - FormulaStrengthening
```
public FormulaStrengthening(List<String> literals,
                            int strengthening_rate,
                            int num_of_strengthening_to_apply)
```
    Creates a strengthening visitor over the given variable alphabet.
    
    Parameters:
    
    literals - the specification's variable names, in index order
    
    strengthening_rate - per-node mutation probability is 1/strengthening_rate
    
    num_of_strengthening_to_apply - maximum number of sub-formulas this visitor may strengthen 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 strengthen (should be in negation normal form)
    
    Returns:
    
    the (possibly) strengthened formula
  - visit
```
public owl.ltl.Formula visit(owl.ltl.BooleanConstant booleanConstant)
```
    Strengthens a boolean constant: true ⤳ false (the only possible strengthening of a constant; false is already the strongest 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)
```
    Strengthens an atomic literal p into one of, chosen uniformly at random: false (option 0); p ∧ q for a fresh literal q (option 1 — Table 4.1's "add conjunct" rule); or G(p) (option 2 — "always" is stronger than "now").
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.XOperator xOperator)
```
    Strengthens X(a) (recursing into a first) into one of: false (option 0, default); G(a) (option 1 — "always" from the next step on is stronger than a single "next"); or, when a is itself G(b), simplifying X G(b) down to G(b) (option 2 — equivalent, since "always from the next step" already implies "always").
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.FOperator fOperator)
```
    Strengthens F(a) (recursing into a first) into one of, drawn uniformly out of 8 outcomes: false (option 0); a itself (option 1 — requiring it now rather than eventually); X(a) (option 2 — requiring it at the very next step); G(a) (option 3 — requiring it forever, Table 4.1's strongest "eventually" tightening); F X(a) (option 4, guarded against runaway size — delaying by exactly one step); F G(a) (option 5, same guard — "eventually always", strictly implying plain "eventually"); G F(a) (option 6, same guard — "infinitely often" is the valid strengthening direction of "eventually always", the mirror of FormulaWeakening.visit(GOperator)'s weakening of G F down to F G); or a U b for a drawn literal b (option 7 — requiring a to hold at least until some point, rather than merely eventually).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.GOperator gOperator)
```
    Strengthens G(a) (recursing into a first) into one of, drawn uniformly out of 5 outcomes: false (option 0, default); distributing over a disjunction, G(a1 ∨ a2) ⤳ G(a1) ∨ G(a2) (option 1, only when a is a disjunction, via the disjunctive normal form of the operand — each disjunct is required to hold forever on its own, rather than the weaker requirement that some disjunct hold at each step); G F(b) ⤳ F G(b) (option 2, when a = F(b) — the valid strengthening direction noted above); simplifying G X(b) down to G(b) (option 3, when a = X(b) — equivalent, since "always" already covers the next step); or simplifying the (already-idempotent) G G(b) down to G(b) (option 4, when a is itself a G-formula — a non-strict, equivalence-preserving simplification rather than a proper strengthening).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.Conjunction conjunction)
```
    Strengthens a conjunction a1 ∧ ... ∧ an (recursing into every conjunct first) into one of: false (option 0); adding one more conjunct drawn from the alphabet, a1 ∧ a2 ⤳ a1 ∧ a2 ∧ c (option 1 — a conjunction can only become more demanding by adding conjuncts); or, when not already temporally heavy, G(a1 ∧ ... ∧ an) (option 2 — requiring the whole conjunction to hold forever rather than just now).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.Disjunction disjunction)
```
    Strengthens a disjunction a1 ∨ ... ∨ an (recursing into every disjunct first) into one of: false (option 0); turning the whole disjunction into a conjunction, a1 ∨ a2 ⤳ a1 ∧ a2 (option 1 — Table 4.1's "conjunct" rule); dropping one randomly chosen disjunct, a1 ∨ a2 ⤳ a1 (option 2 — narrowing which alternative is allowed); or, when not already temporally heavy, G(a1 ∨ ... ∨ an) (option 3 — requiring the disjunction to hold forever rather than just now).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.UOperator uOperator)
```
    Strengthens a U b (recursing into both sides first) via its unrolling a U b ≡ b ∨ (a ∧ ¬b ∧ X(a U b)), into one of: false (option 0); b (option 1 — requiring the eventual condition to hold now, dropping the "until" build-up entirely); or, when not already temporally heavy, a ∧ ¬b ∧ X(a U b) (option 2 — unrolling one step: a must hold now, b must not yet, and the same obligation continues from the next step).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.WOperator wOperator)
```
    Strengthens a W b (recursing into both sides first). Recalling a W b ≡ G(a) ∨ (a U b), this collapses the disjunction to one side rather than weakening it: false (option 0); G(a) (option 1 — keeping only the "always" disjunct); or a U b (option 2 — keeping only the "until" disjunct, which additionally requires b to eventually hold — strictly stronger than the original weak-until).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.MOperator mOperator)
```
    Strengthens a M b ("strong release" — via the standard duality a M b ≡ b U (a ∧ b), and its own unrolling ≡ (a ∧ b) ∨ (b ∧ ¬(a ∧ b) ∧ X(b U (a ∧ b))) — recursing into both sides first) into one of: false (option 0); a ∧ b (option 1 — requiring the joint condition to hold now, the strongest immediate reading); or b ∧ ¬(a ∧ b) ∧ X(a M b) (option 2 — unrolling one step of the "strong release" obligation).
    
    Specified by:
    
    visit in interface owl.ltl.visitors.Visitor<owl.ltl.Formula>
  - visit
```
public owl.ltl.Formula visit(owl.ltl.ROperator rOperator)
```
    Strengthens a R b ("release" — via the standard duality a R b ≡ b W (a ∧ b) ≡ G(b) ∨ (a M b) — recursing into both sides first) into one of: false (option 0); G(b) (option 1 — keeping only the "always b" disjunct); or a M b (option 2 — keeping only the "strong release" disjunct, strictly stronger than the original release).
    
    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 strengthened. Mirrors FormulaWeakening.new_literal(Formula): tries (up to 5 attempts) to avoid a variable already appearing in current, then negates the result with 50% probability. Not a logically fresh Skolem variable — see the class-level soundness caveat.
    
    Parameters:
    
    current - the formula being strengthened, used only to bias the draw away from its own propositions
    
    Returns:
    
    a literal (possibly negated) from the variable alphabet

Class FormulaStrengthening

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Methods inherited from interface java.util.function.Function

Constructor Detail

FormulaStrengthening

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