Package geneticalgorithm

Class SpecificationGeneticAlgorithm

  • public class SpecificationGeneticAlgorithm
extends Object
    Main entry point of the AuRUS search: a genetic algorithm that evolves candidate repairs for an unrealisable assume-guarantee LTL specification.

    Given an input Tlsf specification S = (A, G), this class orchestrates the complete evolutionary loop:

    1. Initial population — seeded from the original specification plus variants obtained by adding patterned assumptions over the input variables (e.g. G F x, G !(x0 & ... & xn)) and by lightly mutating individual assumptions and guarantees (see createInitialPopulation(Tlsf)).
    2. Fitness evaluation — each candidate is scored by AutomataBasedModelCountingSpecificationFitness, which combines the realisability status (checked with Strix), the syntactic similarity, and the semantic similarity (estimated via bounded model counting over automaton transfer matrices) with respect to the original specification.
    3. Evolution — selection, crossover and mutation are applied over successive generations, with rates and budgets taken from Settings (population size, crossover/mutation rates, maximum number of individuals, generations, and overall timeout).
    4. Output — every candidate that reaches full realisability is collected into solutions and reported, ranked by fitness, in TLSF format.

    This class implements the approach introduced in: 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 build on the technique.

    Author:
    Matías Brizzio
    See Also:
    SpecificationChromosome, AutomataBasedModelCountingSpecificationFitness, Settings

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      String print_config()
      Returns a one-line summary of the current genetic-algorithm configuration: generations, population size, individuals budget, mutation rate and crossover rate.
      String print_execution_time()
      Returns a summary of the wall-clock time spent by the run: the search time (initial population until the end of the evolution) and the total time (until solutions were printed), both in seconds.
      void run​(owl.ltl.tlsf.Tlsf spec)
      Runs the genetic search on the given specification using the fitness weights currently configured in Settings (equivalent to calling run(Tlsf, double, double, double) with negative factors, which leaves the configured values untouched).
      void run​(owl.ltl.tlsf.Tlsf spec, double status_factor, double syntactic_factor, double semantic_factor)
      Runs the complete genetic search on the given specification.
      void runRandom​(owl.ltl.tlsf.Tlsf spec)
      Baseline used in the experimental evaluation (flag -random): instead of evolving the population, it generates Settings.GA_POPULATION_SIZE random mutants of the input specification and checks each one for realisability with Strix at the end.

    • Field Detail

      • initialExecutionTime

        public Instant initialExecutionTime
        Timestamp taken when the run starts, before building the initial population.

      • searchExecutionTime

        public Instant searchExecutionTime
        Timestamp taken when the evolutionary search finishes (before the final realisability sweep).

      • finalExecutionTime

        public Instant finalExecutionTime
        Timestamp taken at the very end of the run, after solutions have been printed.

      • bestSolutions

        public List<SpecificationChromosome> bestSolutions
        Best candidates collected during the search when realisability is not checked inside the fitness (see Settings.check_REALIZABILITY and Settings.check_STRONG_SAT). These are verified with Strix in a final sweep and promoted to solutions if realisable.

    • Constructor Detail

      • SpecificationGeneticAlgorithm

        public SpecificationGeneticAlgorithm()

    • Method Detail

      • run

        public void run​(owl.ltl.tlsf.Tlsf spec)
         throws IOException,
                InterruptedException
        Runs the genetic search on the given specification using the fitness weights currently configured in Settings (equivalent to calling run(Tlsf, double, double, double) with negative factors, which leaves the configured values untouched).
        Parameters:
        spec - the (typically unrealisable) input specification to repair
        Throws:
        IOException - if an external solver invocation fails
        InterruptedException - if an external solver call is interrupted

      • run

        public void run​(owl.ltl.tlsf.Tlsf spec,
                double status_factor,
                double syntactic_factor,
                double semantic_factor)
         throws IOException,
                InterruptedException
        Runs the complete genetic search on the given specification.

        The three factors set the weights of the fitness components (realisability status, syntactic similarity, semantic similarity); they are forwarded to Settings.setFactors(double, double, double) and should sum to 1. Passing a negative value keeps the currently configured weight for that component.

        The method aborts early (without searching) if the input specification is already realisable, or if it is inconsistent — the approach requires a consistent specification as input. On termination, all realisable repairs found are printed in TLSF format together with timing and configuration information.

        Parameters:
        spec - the (typically unrealisable) input specification to repair
        status_factor - weight of the realisability-status component of the fitness
        syntactic_factor - weight of the syntactic-similarity component of the fitness
        semantic_factor - weight of the semantic-similarity (model counting) component of the fitness
        Throws:
        IOException - if an external solver invocation fails
        InterruptedException - if an external solver call is interrupted

      • runRandom

        public void runRandom​(owl.ltl.tlsf.Tlsf spec)
               throws IOException,
                      InterruptedException
        Baseline used in the experimental evaluation (flag -random): instead of evolving the population, it generates Settings.GA_POPULATION_SIZE random mutants of the input specification and checks each one for realisability with Strix at the end. No fitness guidance is used, so comparing this baseline against run(Tlsf) isolates the contribution of the guided search.
        Parameters:
        spec - the (typically unrealisable) input specification
        Throws:
        IOException - if an external solver invocation fails
        InterruptedException - if an external solver call is interrupted

      • print_config

        public String print_config()
        Returns a one-line summary of the current genetic-algorithm configuration: generations, population size, individuals budget, mutation rate and crossover rate.
        Returns:
        a human-readable configuration string

      • print_execution_time

        public String print_execution_time()
        Returns a summary of the wall-clock time spent by the run: the search time (initial population until the end of the evolution) and the total time (until solutions were printed), both in seconds. Relies on the timestamps initialExecutionTime, searchExecutionTime and finalExecutionTime.
        Returns:
        a human-readable timing string