Package geneticalgorithm

Class SpecificationChromosome

java.lang.Object

geneticalgorithm.SpecificationChromosome

All Implemented Interfaces:

com.lagodiuk.ga.Chromosome<SpecificationChromosome>, Cloneable

public class SpecificationChromosome
extends Object
implements com.lagodiuk.ga.Chromosome<SpecificationChromosome>, Cloneable

The individual of AuRUS's genetic search: a complete assume-guarantee specification, together with its cached evaluation results.

A chromosome is not a single formula but a full Tlsf specification (A', G'); the genes are the sub-formulas of its assumptions and guarantees, and the genetic operators — crossover(SpecificationChromosome) and mutate() — act directly on their syntax trees. Alongside the specification, the chromosome caches the results of its (expensive) evaluation: the realisability status, the fitness value, and the syntactic and semantic distances to the original specification, all filled in by AutomataBasedModelCountingSpecificationFitness and read back by the search loop so that no candidate is ever evaluated twice.

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:

SpecificationGeneticAlgorithm, SpecificationMutator, SpecificationCrossover, AutomataBasedModelCountingSpecificationFitness

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	SpecificationChromosome.SPEC_STATUS	The evaluation lattice of a candidate specification, ordered from completely broken to repaired:

Field Summary

Fields

Modifier and Type	Field	Description
double	fitness	Cached fitness value, filled in when the chromosome is evaluated.
double	semantic_distance	Cached semantic similarity to the original specification, in [0, 1].
owl.ltl.tlsf.Tlsf	spec	The assume-guarantee specification this individual represents.
SpecificationChromosome.SPEC_STATUS	status	Cached realisability status, computed lazily by the fitness function.
double	syntactic_distance	Cached syntactic similarity to the original specification, in [0, 1].

Constructor Summary

Constructors

Constructor	Description
SpecificationChromosome()	Creates an empty chromosome with no specification (used internally).
SpecificationChromosome(owl.ltl.tlsf.Tlsf spec)	Creates a chromosome for the given specification.

Method Summary

Modifier and Type	Method	Description
SpecificationChromosome	clone()	Shallow clone (the specification reference is shared, not copied).
List<SpecificationChromosome>	crossover(SpecificationChromosome anotherChromosome)	Recombines this individual with another parent, producing offspring that mix assumptions and guarantees from both.
boolean	equals(Object obj)	Semantic-leaning equality used to deduplicate candidates (e.g.
int	hashCode()	Hash consistent with equals(Object), combining the specification, the status and the fitness.
SpecificationChromosome	mutate()	Produces a mutated copy of this individual by delegating to SpecificationMutator, which selects an assumption or a guarantee (biased by -GPR), picks a random sub-formula inside it, and rewrites it with one of the three mutation modes (general, weakening, strengthening).

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, toString, wait, wait, wait

Field Detail

spec

public owl.ltl.tlsf.Tlsf spec

The assume-guarantee specification this individual represents.

status

public SpecificationChromosome.SPEC_STATUS status

Cached realisability status, computed lazily by the fitness function. SpecificationChromosome.SPEC_STATUS.UNKNOWN until the chromosome is evaluated.

fitness

public double fitness

Cached fitness value, filled in when the chromosome is evaluated.

syntactic_distance

public double syntactic_distance

Cached syntactic similarity to the original specification, in [0, 1].

semantic_distance

public double semantic_distance

Cached semantic similarity to the original specification, in [0, 1].

Constructor Detail

SpecificationChromosome

public SpecificationChromosome()

Creates an empty chromosome with no specification (used internally).

SpecificationChromosome

public SpecificationChromosome(owl.ltl.tlsf.Tlsf spec)

Creates a chromosome for the given specification.

The specification is round-tripped through its TLSF textual form (TlsfParser.parse(TlsfUtils.toTLSF(spec))): this produces a normalised deep copy, so chromosomes never share formula structure with one another — a mutation applied to one individual can never leak into a sibling. The status starts as SpecificationChromosome.SPEC_STATUS.UNKNOWN, marking the chromosome as not yet evaluated.

Parameters:

spec - the specification this individual should represent

Method Detail

crossover

public List<SpecificationChromosome> crossover(SpecificationChromosome anotherChromosome)

Recombines this individual with another parent, producing offspring that mix assumptions and guarantees from both.

For each side (assumptions, guarantees) a recombination level is drawn uniformly from {0, 1, 2} and the pair is handed to SpecificationCrossover.apply(Tlsf, Tlsf, int, int):

• level 0 — the whole side is inherited from one randomly chosen parent (a wholesale swap, no mixing);
• level 1 — the side is a random merge of conjuncts drawn from both parents;
• level 2 — sub-formulas of the two parents are combined at the syntax-tree level (transplanting or merging sub-trees), the deepest form of mixing.

The guarantee-preference factor (Settings. GA_GUARANTEES_PREFERENCE_FACTOR, flag -GPR) biases where the interesting recombination happens: with probability GPR% the assumption side is forced to level 0 (inherited wholesale) so the guarantees carry the mixing, and with the complementary probability the guarantee side is forced to level 0 instead.

Specified by:

crossover in interface com.lagodiuk.ga.Chromosome<SpecificationChromosome>

Parameters:

anotherChromosome - the second parent

Returns:

the offspring produced by the crossover (possibly several)

mutate

public SpecificationChromosome mutate()

Produces a mutated copy of this individual by delegating to SpecificationMutator, which selects an assumption or a guarantee (biased by -GPR), picks a random sub-formula inside it, and rewrites it with one of the three mutation modes (general, weakening, strengthening).

Specified by:

mutate in interface com.lagodiuk.ga.Chromosome<SpecificationChromosome>

Returns:

a fresh chromosome carrying the mutated specification, or null if the mutator could not produce a valid mutant

hashCode

public int hashCode()

Hash consistent with equals(Object), combining the specification, the status and the fitness.

Caveat: fitness and status are mutable and change when the chromosome is evaluated, so the hash of an individual is not stable across evaluation. Chromosomes should not be stored in hash-based collections before their evaluation has settled; the search itself only relies on list membership (contains), which uses equals directly.

Overrides:

hashCode in class Object

equals

public boolean equals(Object obj)

Semantic-leaning equality used to deduplicate candidates (e.g. in the solutions list): two chromosomes are equal when their specifications are syntactically equivalent after simplification — both formulas are normalised with SyntacticSimplifier and compared — and, if both individuals have already been evaluated (fitness > 0), their fitness values and statuses also agree. Comparing the simplified forms means trivially different spellings of the same specification (reordered conjuncts, double negations, ...) count as the same individual.

Overrides:

equals in class Object

clone

public SpecificationChromosome clone()

Shallow clone (the specification reference is shared, not copied).

Overrides:

clone in class Object