DOI: 10.5281/zenodo.15271848
title: Artifact for (Semantic) Feature Model Differences with (Q)SAT

description: Author Information



Names: Simone Heisinger, Maximilian Heisinger, Martina Seidl

Affiliations: Johannes Kepler University Linz, Institute for Symbolic AI

Emails: simone.heisinger@jku.at, maximilian.heisinger@jku.at, martina.seidl@jku.at


Associated Paper Information



Title: (Semantic) Feature Model Differences with (Q)SAT

Abstract: Feature models evolve in multiple iterations over time. When modellers change a model, they enact syntactical changes in order to produce specific semantic differences between model iterations. Many tools have been developed to analyze such syntactical differences, but the changing semantics of models were harder to assess. Tools for semantic differences between feature model iterations rely on Binary Decision Diagrams (BDDs) or encode each change into SAT, the former leading to BDD scaling issues and the latter requiring editor support or other specialized tooling. We contribute the first concise formalization of feature models and their semantic differences into propositional logic and use it to efficiently and scalably classify semantic differences using SAT solvers. We then extend our definition into QSAT in order to quantify the full list of semantic differences between feature models and enumerate them using QBF tools, without needing specialized feature model solvers. We implement a semantic difference classifier using our UVL processing pipeline based on Booleguru (instead of the more widely used FeatureIDE) and evaluate it on industrial feature model instances in the standardized UVL format. We also evaluate our QSAT-based semantic difference enumerator and reproduce prior results. We provide all software and evaluation results in an artifact.


Documentation

The code comes from these upstream repositories:



https://gitlab.sai.jku.at/booleguru/booleguru

https://gitlab.sai.jku.at/maximaximal/outer-count

https://github.com/arminbiere/kissat

https://github.com/lonsing/depqbf


The artifact contains:



the necessary software to run the experiments (booleguru, outercount, kissat, compare.sh)

a script quick-test.sh to see if all software is correctly installed

test-formula-uvl.uvl and test-formula-dimacs.dimacs which are needed for quick-test.sh

the scripts reproduce-table1.sh, reproduce-table2.sh, reproduce-table3.sh and reproduce-table4.sh to generate the output from the corresponding tables in the paper (Semantic) Feature Model Differences with (Q)SAT

in bigfiles/ are all .uvl files used in the evaluation (original files can also be downloaded from uvlhub.io). The modified versions of each formula are names _mov.uvl which indicate that some part of the formula was moved

applet1.uvl and applet2.uvl represent the running example from the paper Feature Model Differences from 2012

bike1.uvl and bike2.uvl represent the running example from our paper

when using the sources without docker, we provide the compiled binaries for x64 Linux in bin-linux-amd64. This also includes a setup-path.sh script to set the $PATH variable. For more detailed information on this see our DETAILS.html.

the results (classifications and runtimes) for table 3 in the paper from the original run. For more detailed information on this see the DETAILS.html

a DETAILS.org/DETAILS.html with more detailed information on the commands used in the scripts: DETAILS.html, its markup version is in DETAILS.org.

a Dockerfile to run the software and tests in, using Docker, Podman, or some other software.




Artifact Evaluation Environment

System Specifications Used by Authors



Operating System: Ubuntu 24.04

CPU: AMD EPYC 7313

Memory: 256 GB

Disk Space: 10 GB

GPU (if applicable): none


Estimated Hardware Requirements for Evaluation



Minimum required CPU: any

Minimum required Memory: 8 GB

Minimum required Disk Space: 10 GB

Minimum required GPU (if applicable): none


Software Requirements



Podman or Docker (the former often is readily available in package repositories)


Compatibility Considerations



Known compatibility issues of the container/VM: Untested on Windows


Kick-the-Tires

To run the container with the provided zst using Podman:



podman load < fmdiff-container.tar.zst
podman run -ti --replace --name fmdiff localhost/fmdiff


To fully rebuild the container, use the following:



podman build . -t fmdiff
podman run -ti --replace --name fmdiff localhost/fmdiff


If opening the provided container, change your directory into artifact using cd artifact before running the mentioned scripts.

To check all tools if they are working correctly after the setup, run the provided script ./quick-test.sh.

There, all tools should display some output. The correct output is provided directly after the tool's output. Please confirm if the tool output and the expected output match. The output could be out of order, this has no impact on the functionality of the artifact.

the checks included in quick-test.sh are:



booleguru working test

kissat working test

outercount working test

compare.sh working test


For the bigger evaluations, increase the stack size using ulimit -s 800000. This is done automatically in the reproduce-table3.sh script, but has to be done manually once for each terminal session if you decide to do further evaluations.

If booleguru is aborting with errors, most likely the stack size was too small, which happens if it stays at the default. The error comes from the kernel not allowing booleguru's stack to grow forever. Booleguru's design has some recursive functions that need a bigger stack size for some operations.

Full Evaluation

If opening the provided container, change your directory into artifact using cd artifact before running the mentioned scripts.

Table 1

To reproduce table 1 from the paper (configurations which are allowed in bike2 but not in bike1):

run the script reproduce-table1.sh with ./reproduce-table1.sh

This prints the 4 configurations mentioned in the paper in table 1. NOTE: the lines in the table featured in the paper are rearranged and for better human reading include some spacing. The output from this script contains the same information as in the table in the paper.

The estimated runtime is less than a few seconds.

Table 2

To reproduce table 2 from the paper (configurations which are allowed in bike1 but not in bike2):

run the script reproduce-table2.sh with ./reproduce-table2.sh

This prints the 5 configurations mentioned in the paper in table 2. NOTE: the lines in the table featured in the paper are rearranged and for better human reading include some spacing. The output from this script contains the sam information as in the table in the paper.

The estimated runtime is less than a few seconds.

Table 3

To reproduce table 3 from the paper (times to classify edits and if a classification applies):

run the script reproduce-table3.sh with ./reproduce-table3.sh

This prints for every feature model name mentioned in table 3 in the paper the classification and how long it took to get that classification. So each cell from the paper is printed with the script like this:



============================================
= automotive01
============================================

=== automotive01 generalization ===
booleguru "!(" "bigfiles/automotive01.uvl" "<-" "bigfiles/automotive01_mov.uvl" ")" --dimacs
bigfiles/automotive01.uvl <- bigfiles/automotive01_mov.uvl ===== 1
bigfiles/automotive01.uvl is not a generalization of bigfiles/automotive01_mov.uvl

real	0m1,507s
user	0m1,486s
sys	0m0,019s


From this we can see that for automotive01 it checks if it is a generalization or not. The last line of text says bigfiles/automotive01.uvl is not a generalization of bigfiles/automotive01_mov.uvl so it is not a generalization. The time which is important for the table is real 0m1,507s. Times can change depending on used hardware, the important part is that for the strict-generalization and strict-specialization the runtime should be around double that of the non strict version if the non strict check holds. This means that for automotive01 and financialservices01 since generalization and specialization do not hold, all five times should be around the same. For all other names in the table (automotive02_01, automotive02_02, automotive02_03, automotive02_04, ea2468, linux-2.6.33.3) strict-generalization and strict-specialization should take around double the time generalization and specialization take. Relative differences between the files should be similar compared to in the paper.

The estimated runtime depends on the hardware used, with a regular laptop with a recent Intel CPU and 16GB of RAM the whole script runs for about 5 minutes.

In the folder results are the times with the tested setup which are the times mentioned in the paper.

Table 4

To reproduce table 4 from the paper (configurations which are allowed in applet1 but not in applet2):

run the script reproduce-table4.sh with ./reproduce-table4.sh

This prints the 4 configurations mentioned in the paper in table 4.

The estimated runtime is less than a few seconds.