The Tool

In this page, you can find the instructions to reproduce the experiments performed as part of the paper "Goal-Conflict Likelihood Assessment based on Model Counting" submitted to ICSE 2018. 

Installation Instructions

REQUIREMENTS

• • Java 8.

• The string model counter ABC. 

• GNU Plot.

DOWNLOAD

You can download the tool from this link: LTLmodelcounting.

INSTALL

• Follow ABC instructions to install the string model counter. 

  • NOTE: It is very important to use the versions they recommend for each dependence: Ubuntu 16.04, Flex 2.6.0 and Bison 3.0.4. 

  • We recommend to use the Step-by-Step Setup.

• To compile our tool run: ant compile. 

  • We provide an Ant script (build.xml file) and the libraries required (LamaConv and JFLAP) into the lib folder.  

  • Install GNU Plot in order to generate the plotting progressions for each case study.

RUNNING EXPERIMENTS

• • We provide the script run-case-studies.sh in order to reproduce all the experimental evaluation.

  • In the folder case-studies you can find the specifications and the results of each case study.

  • To generate the plotting progressions:

• 1. First,  use the scripts plot.sh and plot-goal-satisfaction.sh to calculate the progressions for each experiment.

  2. Second, move to the plot/plot-goal-satisfaction folder, and run: gnuplot case-study.mp. 

     1. For instance, into the folder plot/minepump, run: gnuplot minepump.gp.

READING THE RESULTS

Go to the Results section to find a brief analysis of the obtained results.