Artifact for (Semantic) Feature Model Differences with (Q)SAT

Author Information Names: Simone Heisinger, Maximilian Heisinger, Martina Seidl Affiliations: Johannes Kepler University Linz, Institute for Symbolic AI Emails: [e-mail], [e-mail], [e-mail] 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 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 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 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. error: booleguru cannot execute an operation -> the command ulimit -s 800000 was not executed before running the reproduce table scripts. 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.