Package geneticalgorithm

Class AutomataBasedModelCountingSpecificationFitness

  • All Implemented Interfaces:
    com.lagodiuk.ga.Fitness<SpecificationChromosome,​Double>
    public class AutomataBasedModelCountingSpecificationFitness
extends Object
implements com.lagodiuk.ga.Fitness<SpecificationChromosome,​Double>
    The multi-objective fitness function of AuRUS — the compass that guides the genetic search — with the semantic component estimated via approximate bounded model counting over automaton transfer matrices.

    Given the original specification S and a candidate repair S', the fitness is the weighted sum

       f(S') = STATUS_FACTOR      * status(S')
         + LOST_MODELS_FACTOR * lost(S, S')
         + WON_MODELS_FACTOR  * won(S, S')
         + SYNTACTIC_FACTOR   * synSim(S, S')

    where the weights come from Settings (flag -factors; the semantic weight is split evenly between the lost-models and won-models directions) and:

    • status(S') rewards progress towards a well-formed, realisable specification on a graded ladder, so partially fixed candidates still receive gradient (see getStatusFitness(SpecificationChromosome));
    • lost(S, S') is the fraction of the original specification's behaviours preserved by the candidate, computed as 1 - #(S &and; &not;S', k) / #(S, k) (see compute_lost_models_porcentage(Tlsf, Tlsf));
    • won(S, S') penalises the new behaviours the candidate introduces, computed as 1 - #(&not;S &and; S', k) / #(S', k) (see compute_won_models_porcentage(Tlsf, Tlsf));
    • synSim(S, S') is the sub-formula overlap between the two specifications (see compute_syntactic_distance(Tlsf, Tlsf)).

    All model counts #(&phi;, k) are numbers of satisfying traces of bounded length k (Settings.MC_BOUND, flag -k), approximated by EmersonLeiAutomatonBasedModelCounting: the formula is translated into an automaton, the automaton is encoded as a transfer matrix T whose entries count the propositional valuations on each transition, and the count is obtained by matrix exponentiation as I &middot; T^k &middot; F. The approximation preserves the relative ordering of candidates — which is all the search needs — at a small fraction of the cost of exact counting.

    Note on formulation: the paper presents the semantic similarity in its positive form (via the shared models #(S &and; S', k)); this implementation computes the algebraically equivalent complement form (via the lost and won models). The equivalence follows from partitioning the models of each specification, and is documented in detail — with worked examples and the design rationale — in docs/FITNESS.md.

    This fitness design (graded realisability status + syntactic similarity + model-counting-based semantic similarity) is the central contribution of: M. Brizzio, M. Cordy, M. Papadakis, C. Sánchez, N. Aguirre, R. Degiovanni. "Automated Repair of Unrealisable LTL Specifications Guided by Model Counting", GECCO 2023 (doi:10.1145/3583131.3590454). Please cite this paper if you reuse or reimplement the technique. The paper presents the semantic similarity through the shared-models ratios #(S &and; S')/#(S) and #(S &and; S')/#(S'); the complement form computed here is algebraically equivalent — see docs/FITNESS.md for the derivation and its numerical verification.

    Author:
    Matías Brizzio
    See Also:
    SpecificationGeneticAlgorithm, SpecificationChromosome, EmersonLeiAutomatonBasedModelCounting, Settings

    • Field Summary

      Fields 
      Modifier and Type Field Description
      List<String> alphabet
      Atomic propositions of the specification (currently unused; kept for compatibility).
      BigInteger originalNumOfModels
      Bounded model count #(S, k) of the original specification, computed once at construction time (only when the lost-models component is active).
      owl.ltl.tlsf.Tlsf originalSpecification
      The original (typically unrealisable) specification every candidate is compared against.
      SpecificationChromosome.SPEC_STATUS originalStatus
      Status of the original specification, computed once at construction time.

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      Double calculate​(SpecificationChromosome chromosome)
      Computes the fitness of a candidate repair (the weighted sum described in the class documentation).
      double compute_semantic_distance​(owl.ltl.tlsf.Tlsf original, owl.ltl.tlsf.Tlsf refined)
      Semantic similarity between two specifications, as the even average of the lost-models and won-models components: 0.5 * lost + 0.5 * won.
      void compute_status​(SpecificationChromosome chromosome)
      Computes and stores the SpecificationChromosome.SPEC_STATUS of a candidate, performing the satisfiability/realisability analysis that feeds the status ladder.
      double compute_syntactic_distance​(owl.ltl.tlsf.Tlsf original, owl.ltl.tlsf.Tlsf refined)
      Syntactic similarity between two specifications: the even average of the two sub-formula overlap ratios, 0.5 * |SF(S) &cap; SF(S')| / |SF(S)| + 0.5 * |SF(S) &cap; SF(S')| / |SF(S')|.
      void print_config()
      Prints the active fitness configuration to standard output: the four component weights (status, lost models, won models, syntactic) and the assumption-addition / guarantee-removal flags.
      boolean somethingHasBeenRemoved​(owl.ltl.tlsf.Tlsf original, owl.ltl.tlsf.Tlsf refined)
      Structural guard used to prune candidates that transgress the configured search space: returns true if the candidate added an assumption while Settings.allowAssumptionAddition is disabled, or removed a guarantee while Settings.allowGuaranteeRemoval is disabled (both detected by comparing conjunct counts against the original specification).

    • Field Detail

      • originalSpecification

        public owl.ltl.tlsf.Tlsf originalSpecification
        The original (typically unrealisable) specification every candidate is compared against.

      • alphabet

        public List<String> alphabet
        Atomic propositions of the specification (currently unused; kept for compatibility).

      • originalNumOfModels

        public BigInteger originalNumOfModels
        Bounded model count #(S, k) of the original specification, computed once at construction time (only when the lost-models component is active). Used as the denominator of the lost-models ratio for every candidate.

    • Constructor Detail

      • AutomataBasedModelCountingSpecificationFitness

        public AutomataBasedModelCountingSpecificationFitness​(owl.ltl.tlsf.Tlsf originalSpecification)
                                               throws IOException,
                                                      InterruptedException
        Creates the fitness function for a given original specification.

        Computes and caches the status of the original specification (printed to standard output) and, if the lost-models component is enabled, its bounded model count #(S, k) — so it is paid once instead of once per candidate.

        Parameters:
        originalSpecification - the specification the search will try to repair
        Throws:
        IOException - if an external solver invocation fails
        InterruptedException - if an external solver call is interrupted

    • Method Detail

      • calculate

        public Double calculate​(SpecificationChromosome chromosome)
        Computes the fitness of a candidate repair (the weighted sum described in the class documentation).

        Degenerate candidates are pruned with fitness 0: candidates identical to the original specification, candidates with a false assumption (vacuously realisable), candidates whose guarantees collapsed to true (the useless "do whatever you want" repair), and candidates that removed guarantees or added assumptions when the corresponding flags forbid it. The lost/won model ratios are only evaluated when both specifications are consistent and the candidate is not syntactically identical to the original; fitness values above the theoretical maximum abort the run, as they indicate a configuration bug.

        As side effects, the computed fitness, syntactic distance and semantic distance are stored in the chromosome, and a previously evaluated chromosome (status different from UNKNOWN) returns its cached fitness immediately.

        Specified by:
        calculate in interface com.lagodiuk.ga.Fitness<SpecificationChromosome,​Double>
        Parameters:
        chromosome - the candidate specification to score
        Returns:
        the fitness value in [0, 1]

      • compute_status

        public void compute_status​(SpecificationChromosome chromosome)
                    throws IOException,
                           InterruptedException
        Computes and stores the SpecificationChromosome.SPEC_STATUS of a candidate, performing the satisfiability/realisability analysis that feeds the status ladder.

        The analysis proceeds bottom-up. The environment side (initially &and; G(require) &and; assume) and the system side (preset &and; G(assert) &and; guarantees) are first checked for satisfiability in isolation, yielding BOTTOM, GUARANTEES or ASSUMPTIONS when one (or both) is unsatisfiable. If both sides are satisfiable, their conjunction is checked: an unsatisfiable conjunction yields CONTRADICTORY. Finally, consistent candidates are checked for realisability — with Strix, or with the potential-realisability (strong satisfiability) check when Settings.check_STRONG_SAT is enabled — yielding REALIZABLE or UNREALIZABLE. Inconclusive solver answers (e.g. timeouts) leave the status as UNKNOWN.

        Chromosomes whose status was already computed are returned untouched, so the (expensive) solver calls are paid at most once per candidate.

        Parameters:
        chromosome - the candidate whose status should be computed
        Throws:
        IOException - if an external solver invocation fails
        InterruptedException - if an external solver call is interrupted

      • compute_semantic_distance

        public double compute_semantic_distance​(owl.ltl.tlsf.Tlsf original,
                                        owl.ltl.tlsf.Tlsf refined)
        Semantic similarity between two specifications, as the even average of the lost-models and won-models components: 0.5 * lost + 0.5 * won. Exposed for reporting purposes (e.g. assessing final solutions against genuine reference repairs); inside the search, calculate(SpecificationChromosome) weights the two directions independently.
        Parameters:
        original - the original specification S
        refined - the candidate repair S'
        Returns:
        the semantic similarity in [0, 1]

      • compute_syntactic_distance

        public double compute_syntactic_distance​(owl.ltl.tlsf.Tlsf original,
                                         owl.ltl.tlsf.Tlsf refined)
        Syntactic similarity between two specifications: the even average of the two sub-formula overlap ratios, 0.5 * |SF(S) &cap; SF(S')| / |SF(S)| + 0.5 * |SF(S) &cap; SF(S')| / |SF(S')|. A value close to 1 means the candidate shares most of its sub-formulas with the original — it will look familiar to the engineer — while a value close to 0 means the syntactic overlap is minimal.
        Parameters:
        original - the original specification S
        refined - the candidate repair S'
        Returns:
        the syntactic similarity in [0, 1]

      • somethingHasBeenRemoved

        public boolean somethingHasBeenRemoved​(owl.ltl.tlsf.Tlsf original,
                                       owl.ltl.tlsf.Tlsf refined)
        Structural guard used to prune candidates that transgress the configured search space: returns true if the candidate added an assumption while Settings.allowAssumptionAddition is disabled, or removed a guarantee while Settings.allowGuaranteeRemoval is disabled (both detected by comparing conjunct counts against the original specification).
        Parameters:
        original - the original specification
        refined - the candidate repair
        Returns:
        true iff the candidate violates the addition/removal restrictions

      • print_config

        public void print_config()
        Prints the active fitness configuration to standard output: the four component weights (status, lost models, won models, syntactic) and the assumption-addition / guarantee-removal flags.