Genetic Algorithm Results

Dataset

You can download the results of our experimental evaluation from this link: Results.zip. 

In there you can find the results reported in the paper for our Genetic Algorithm, as well the evaluation of our new model counting approach.

You can use script read-results.sh to analyse the outcomes on the 10 runs with each configuration. 

E.g., running ./read-results.sh results/result-70-10-20/arbiter/arbiter-genuine will summarise the results obtained for the Arbiter case study, in the 10 runs of our Genetic Algorithm, under a configuration that assigns .7 to the realisability checking property, .1 to the syntactic distance, and .2 to the semantic distance.

Sensitivity Analysis Results

We guide our genetic algorithm by using a multi-objective fitness function that has three key propertites, the realizability status, the syntactic, and semantic distances to the original unrealizable specification.

We study the impact in the effectiveness of our algorithm, when some of the properties are deactivated from the fitness function computation.  We run the algorithm under six different configurations. 

Intuitively, in configurations (Syn+Sem, Syn, Sem) we deactivate the realisability checking in the algorithm, so it is only guided by the syntactic and/or semantic distance (realisability is only checked at the end of the execution, to check which one is a solution); 

on the other hand, in configurations (Real, Real+Syn, Real+Sem) we deactivate the syntactic and/or semantic distance computation from the fitness function. 

The plots report, for each configuration, the average percentage of realisable solutions found per case study, with respect to the best performance of our algorithm previously discussed (with the three factors activated). 

Notice that, by removing the realisability checking, the algorithm behaves pretty similar, or even worse, than random, affecting drastically its effectiveness in finding repairs. 

On the other hand, configurations that use realisability checking (Real, Real+Syn, Real+Sem) considerably improve the effectiveness of the algorithm, being able to find more number of solutions. 

Best Performing Configuration Analysis

Our multi-objective fitness function focuses on three aspects of the candidate solution, namely, the realisability status (alpha), the syntactic (beta) and semantic (gamma) distances to the original unrealisable specification. 

To find the best configuration, we assess the performance of our algorithm under many configurations, by considering values for alpha, beta and gamma, such that alpha + beta + gamma = 1 (i.e., the sum of the tree weights is 100%). 

Then, we organise our unrealisable specifications into two disjoint sets: the development set and the evaluation set. Basically, we randomly selected 6 cases to be part of the development set  (2 from the literature, 1 from SynTech and 3 from SyntComp) and the remaining 15 cases as part of the evaluation set. 

The development set is meant to support us in setting the parameters of our algorithm, with the hope that the best-performing configuration for the development set, will generalize to the evaluation set.  

We observed that realisability checking is crucial for finding quality solutions, and better performance is reached when the weight assigned to the semantic distance is greater than the weight assigned to the syntactic distance. 

Then, the best configuration detected was: alpha=.7, beta=.1 and gamma = .2.