The version of ICEBAR used in the ASE 2022 research paper "ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications" (2.8.1) and the models reported in the paper can be download from here. ICEBAR's repository can be found at https://github.com/saiema/ICEBAR.
Docker, by either installing Docker Desktop for Windows or macOS; or by installing Docker Engine (not available for Windows).
Pulling image drstein/icebar:2.8.1 by executing docker push drstein/icebar:2.8.1 or by using Docker Desktop.
Our experiments were run with 16Gb of memory as maximum memory available for both the test generation tool and ARepair.
To run the docker, the command is docker run -it drstein/icebar:2.8.1.
For information on the content of our replication package and how to run our experiments follow the instructions below.
After downloading ICEBAR-2.8.1.zip, extract the zip file. Inside the ICEBAR-2.8.1 folder there will be the following folders and files:
experiments folder contains ARepair's and Alloy4Fun's benchmarks.
Tools folder contains both ARepair and BeAFix, the second one is used by ICEBAR to generate tests.
ICEBAR-2.8.1.jar, this can be used by executing java -jar ICEBAR-2.8.1.jar <arguments>, use --help to get information about the arguments to use.
icebar.properties, a properties file with the configuration used in our experiments. You can use this file as a template for you own configurations.
icebar_ARepairMode.properties, a properties file to run ARepair once and check the fix against a property-based oracle. The main difference of this configuration with respect to the previous one is the amount of laps (iterations) used, in this case we used 0 laps, this is equivalent to just running ARepair.
icebar-run.sh, this script runs all ICEBAR experiments.
icebar-run-arepair.sh, this script runs all ARepair experiments.
modelsA4F.sh, this script defines all Alloy4Fun's models to use. Variable A4F_CASES can be modified to remove specific cases by prefixing them with the # symbol.
modelsARepair.sh, this script defines all ARepair's models to use. Variable AREPAIR_CASES can be modified to remove specific cases by prefixing them with the # symbol.
Our tool uses .properties files for configuration purposes. The replication package contains two of these files: icebar.properties, which is used to run ICEBAR in an iterative way to try to find a test suite that allows ARepair to return a non-spurious fix; and icebar_ARepairMode.properties which is used to run ARepair only once and check the resulting fix against a property-based oracle. You can use these files as templates to create your own configurations.
Inside both .properties files, and in any new one, the property icebar.tools.arepair.root=Tools/ARepair must be edited to have the full path to that directory, e.g.: for a user bob who downloaded the replication package inside his Download folder, the property should be changed to icebar.tools.arepair.root=/home/bob/Downloads/ICEBAR-2.8.1/Tools/ARepair/.
In order to replicate our ARepair experiments, that is, running ARepair with different input tests configuration (called suites) the script icebar-run-arepair.sh must be executed indicating as parameter which benchmark to use: ./icebar-run-arepair.sh --run-ARepair for ARepair's benchmark; or ./icebar-run-arepair.sh --run-A4F for Alloy4Fun's benchmark.
In order to replicate our ICEBAR experiments, that is, running ARepair with the buggy model and a test suite, checking the returned repair against the oracle, and strengthening the test suite if the fix was spurious to iterate the process again, the script icebar-run.sh must be executed indicating as parameter which benchmark to use: ./icebar-run.sh --run-ARepair for ARepair's benchmark; or ./icebar-run.sh --run-A4F for Alloy4Fun's benchmark.
Note that in the case of Alloy4Fun's benchmark, due to it's size (around two thousand), running all the cases can take more than two weeks on a desktop computer. To perform the experiments over reduced (user selected) cases, modify either modelsA4F.sh or modelsARepair.sh, commenting the cases to ignore inside A4F_CASES or AREPAIR_CASES respectively by prefixing them with the # symbol.
The results are summarized in a .csv file at the experiment's root folder. For example: if the ICEBAR experiments are executed over the Alloy4Fun benchmark (./icebar-run.sh --run-A4F), file summary-A4F-ICEBAR.csv will be created by the script, containing the following information:
model case name | repair result ( correct, not fix found*, exhausted*, spurious*, or timeout) | ICEBAR iteration (0 in case of ARepair mode) | # of test generated | checking and test generation time (ms) | Repair time (ms) | # of calls to the ARepair tool
(*) not fix found and spurious are reported when running in ARepair mode (0 max iterations); exhausted is used when running with at least one iteration.
ICEBAR was developed and is currently maintained by:
Simón Gutiérrez Brida (sgutierrez@dc.exa.unrc.edu.ar | https://github.com/saiema)
Germán Regis (gregis@dc.exa.unrc.edu.ar | https://github.com/gregistecco)
Guolong Zheng (gzheng@cse.unl.edu | https://github.com/guolong-zheng)