Experimental Evaluation 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. 

File summary-per-case.csv gives summarises the results of each case study under the different configurations explored. 

You can also download Repairs-all-runs.zip (3GB) that contains all the repairs generated by our genetic algorithm in each particular run, as well as, a csv file summarising the execution.

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 similarities 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 similarities (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), as well as, the dyntactic and asemantic similarities for the tp 10 ranked solutions.

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.