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 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.### 作者信息 姓名：Simone Heisinger、Maximilian Heisinger、Martina Seidl 所属机构：约翰内斯·开普勒大学林茨分校，符号人工智能研究所（Institute for Symbolic AI） 电子邮箱：[e-mail]、[e-mail]、[e-mail] ### 关联论文信息 标题：基于（Q）可满足性问题的（语义）特征模型差异分析 摘要：特征模型会随时间经历多轮迭代演进。建模人员修改模型时，会通过语法变更来在不同迭代版本的模型间产生特定语义差异。目前已有诸多工具用于分析此类语法差异，但评估模型的语义变更则难度更高。现有用于特征模型迭代间语义差异分析的工具，要么依赖二元决策图（Binary Decision Diagrams, BDD），要么将每一处变更编码为可满足性问题（SAT）：前者会遭遇BDD的规模扩展性问题，后者则需要编辑器支持或其他专用工具。本文首次实现了特征模型及其语义差异到命题逻辑的简洁形式化，并借此借助可满足性求解器（SAT求解器）高效且可规模化地完成语义差异分类。随后，我们将该定义扩展至量化可满足性问题（QSAT），以量化特征模型间所有语义差异的完整列表，并借助量化布尔公式（QBF）工具枚举这些差异，无需依赖专用的特征模型求解器。我们基于Booleguru（而非应用更广泛的FeatureIDE）搭建了UVL处理流水线，实现了一款语义差异分类器，并在标准化通用可变性语言（UVL）格式的工业级特征模型实例上完成了评估。此外，我们还对基于QSAT的语义差异枚举器进行了评估，并复现了此前的研究结果。本成果附带所有软件与评估结果的研究制品。 ### 文档说明 本代码源自以下上游代码仓库： 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 本研究制品（artifact）包含以下内容： 1. 用于运行实验的必要软件（包括booleguru、outercount、kissat与compare.sh） 2. 用于校验所有软件是否正确安装的脚本quick-test.sh，以及该脚本运行所需的测试公式文件test-formula-uvl.uvl与test-formula-dimacs.dimacs 3. 用于复现论文《基于（Q）SAT的（语义）特征模型差异》中对应表格结果的脚本reproduce-table1.sh、reproduce-table2.sh、reproduce-table3.sh与reproduce-table4.sh 4. bigfiles/目录下包含本次评估所用的全部.uvl格式文件（原始文件亦可从uvlhub.io下载）。每个公式的修改版本均以_mov.uvl命名，用以标识该公式的部分内容已被移动 5. applet1.uvl与applet2.uvl对应2012年发表的论文《Feature Model Differences》中的运行示例；bike1.uvl与bike2.uvl对应本文的运行示例 6. 若不使用Docker构建源码，我们在bin-linux-amd64目录中提供了x64架构Linux系统的编译后二进制文件，其中还包含用于配置$PATH环境变量的setup-path.sh脚本。更多详细信息请参阅DETAILS.html文件 7. 包含本文表3对应的原始实验结果（分类结果与运行时长），更多详细信息请参阅DETAILS.html文件 8. 包含用于说明脚本中所用命令的详细文档DETAILS.html与其标记源文件DETAILS.org 9. 包含用于通过Docker、Podman或其他容器工具运行本软件与测试的Dockerfile文件 ### 研究制品评估环境 #### 作者所用系统配置 - 操作系统：Ubuntu 24.04 - CPU：AMD EPYC 7313 - 内存：256 GB - 磁盘空间：10 GB - 图形处理器（若需）：无 #### 评估所需最低硬件配置 - 最低CPU要求：任意型号 - 最低内存要求：8 GB - 最低磁盘空间要求：10 GB - 最低图形处理器要求（若需）：无 #### 软件依赖 Podman或Docker（前者通常可直接通过软件包仓库获取） #### 兼容性说明 已知容器/虚拟机兼容性问题：未在Windows系统上测试 ### 快速试用流程 若需使用Podman加载并运行提供的zst格式容器镜像，请执行以下命令： podman load < fmdiff-container.tar.zst podman run -ti --replace --name fmdiff localhost/fmdiff 如需完全重新构建容器，请执行以下命令： podman build . -t fmdiff podman run -ti --replace --name fmdiff localhost/fmdiff 若启动已提供的容器，请先执行`cd artifact`命令进入artifact目录，再运行前文提及的脚本。 若需校验安装完成后所有工具是否正常工作，请运行提供的脚本`./quick-test.sh`。该脚本运行时所有工具均会输出相关信息，工具输出后会附带标准预期输出，请校验工具输出与预期输出是否一致。输出顺序可能存在混乱，但不会影响研究制品的功能。 quick-test.sh包含以下校验项： - booleguru功能校验 - kissat功能校验 - outercount功能校验 - compare.sh功能校验 如需运行大规模评估，请先执行`ulimit -s 800000`命令调整栈空间大小。reproduce-table3.sh脚本会自动完成该设置，但如果您需要进行额外的评估，则需在每个终端会话中手动执行该命令。 若booleguru因报错终止运行，大概率是栈空间大小不足——即使用了系统默认的栈大小设置。该报错源于内核不允许booleguru的栈无限增长，booleguru的部分递归函数在执行部分操作时需要更大的栈空间。 ### 完整评估流程 若启动已提供的容器，请先执行`cd artifact`命令进入artifact目录，再运行前文提及的脚本。 #### 表格1复现 如需复现论文中的表格1（bike2允许但bike1不允许的配置项），请执行`./reproduce-table1.sh`脚本。该脚本会输出论文表格1中提及的4组配置项。注意：论文中的表格为便于阅读已对行进行重排并添加了空格，本脚本的输出与论文表格包含的信息完全一致。预计运行时长不足数秒。 #### 表格2复现 如需复现论文中的表格2（bike1允许但bike2不允许的配置项），请执行`./reproduce-table2.sh`脚本。该脚本会输出论文表格2中提及的5组配置项。注意：论文中的表格为便于阅读已对行进行重排并添加了空格，本脚本的输出与论文表格包含的信息完全一致。预计运行时长不足数秒。 #### 表格3复现 如需复现论文中的表格3（编辑分类耗时与分类有效性），请执行`./reproduce-table3.sh`脚本。该脚本会输出论文表格3中提及的所有特征模型的分类结果与对应耗时，本脚本会以如下格式输出论文中的每个单元格内容： ============================================ = 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 从该输出中可以看到，针对automotive01，脚本会校验其是否为泛化版本。最后一行文本显示bigfiles/automotive01.uvl并非bigfiles/automotive01_mov.uvl的泛化版本，因此该模型不属于泛化类型。表格中关键的耗时指标为`real 0m1,507s`。运行耗时会因硬件配置不同而有所差异，核心规律为：若非严格校验通过，则严格泛化与严格特化的运行时长约为非严格版本的两倍。这意味着对于automotive01与financialservices01，由于泛化与特化校验均不通过，五项测试的耗时应大致相同。而对于表格中其余名称（automotive02_01、automotive02_02、automotive02_03、automotive02_04、ea2468、linux-2.6.33.3），严格泛化与严格特化的耗时应约为泛化与特化校验的两倍。各文件间的相对耗时差异应与论文中呈现的结果一致。 整体运行耗时取决于所用硬件，在搭载最新英特尔CPU与16GB内存的常规笔记本电脑上，整个脚本的运行时长约为5分钟。results目录下包含本次测试配置下的耗时数据，即论文中提及的实验结果。 #### 表格4复现 如需复现论文中的表格4（applet1允许但applet2不允许的配置项），请执行`./reproduce-table4.sh`脚本。该脚本会输出论文表格4中提及的4组配置项。预计运行时长不足数秒。