Kmax-generated files are corrupt due to a wrong usage of the Z3 API. To prevent usage of these corrupted files, all data has been removed from the current commit of this repository. This repository is only for archiving purposes. Consider using our fixed and improved tool over at tseitin-or-not-tseitin or our curated feature-model benchmark.
This repository provides feature models for a diverse set of variant-rich (software) systems, including open-source projects based on the Kconfig language for variability modeling and others, which are mainly intended for the evaluation of product-line analysis techniques.
The repository contains two kinds of feature models:
- First, feature models that were generated by our feature-model-repository-pipeline (for technical details, see that repository). In short, these models were mined from Kconfig-based projects using kconfigreader and Kmax/Kclause.
- Second, feature models that were used in various publications from the product-line community. All such models were added with permission from the original authors, which we credit below.
For generated models, we provide some statistics in CSV files (see below); models from publications are added as is.
To filter models (e.g., to select models for an evaluation), we recommend to use standard Unix tools (e.g., find . | grep \\.kconfigreader\\.model$ > models.txt).
The resulting models.txt is designed to work out-of-the-box with next-gen FeatureIDE.
The file structure of this repository is as follows:
models/ feature model files
<system>/ linux, busybox, etc.
<identifier>.<source>.<ext> <identifier> is usually a Git tag/commit (or "unknown" for unknown versions)
<source> is kconfigreader/kmax (for generated models) or a publication
for <ext>, see https://github.com/ekuiter/feature-model-repository
c-bindings/ tools used by kconfigreader/kmax to read feature models
<system>/ linux, busybox, etc.
<identifier>.<binding> <identifier> is usually a Git tag/commit
<binding> is dumpconf/kextractor
read_<tool>.csv table that lists all generated models with tags
eval_<tool>.csv table that includes some basic data about generated models
We supply the following file formats (not all formats are available for all feature models):
*.rsf Intermediate file output by dumpconf (input for kconfigreader)
*.kclause Intermediate file output by kextractor (input for Kclause)
*.features Text file with all feature names
*.kconfigreader.model Text file with Boolean constraints (unprocessed, therefore not necessarily in CNF)
*.kmax.model Serialized binary file with constraints (translated into smtlib2 format, not necessarily in CNF)
*.xml FeatureIDE XML feature model file (may contain a feature hierarchy, not necessarily in CNF)
*.dimacs Standard DIMACS text file with Boolean constraints in Tseytin-transformed CNF (created with kconfigreader or Kmax/Z3)
For generated models, we supply the following tags in CSV files to simplify filtering:
features a .features file is available
model a .model file is available
dimacs a .dimacs file is available
cnf a CNF is available (currently, only as DIMACS)
tseytin the CNF was generated using Tseytin transformation
kmax the model was generated using kmax
kclause a .kclause file is available
kconfigreader the model was generated using kconfigreader
rsf a .rsf file is available
These are the sources for models from publications/tools:
featureide FeatureIDE example feature models
https://github.com/FeatureIDE/FeatureIDE/tree/master/plugins/de.ovgu.featureide.examples/featureide_examples/FeatureModels
knueppel2017 Knueppel et al. 2017: Is There a Mismatch Between Real-World Feature Models and Product-Line Research?
https://github.com/AlexanderKnueppel/is-there-a-mismatch
Kconfig models were read using an extended version of LVAT and translated into FeatureIDE XML files
sundermann2020 Sundermann et al. 2020: Evaluating #SAT solvers on industrial feature models
https://github.com/SoftVarE-Group/emse21-evaluation-sharpsat
DIMACS files were read with FeatureIDE 3.5.5 based on the XMLs from knueppel2017 and others
pett2021 Pett et al. 2021: AutoSMP: An Evaluation Platform for Sampling Algorithms
https://github.com/TUBS-ISF/soletta-case-study
model and DIMACS files read by Smarch/Kclause, XML imported in FeatureIDE from DIMACS