VM2BOOL converts feature models (SPLOT SXFM, Linux Kconfig, eCos CDL) into propositional formulas (DIMACS).
You can obtain SPLOT feature models from http://splot-research.org or Kconfig and CDL models from https://bitbucket.org/tberger/variability-models . Alternatively, derive your own models from the original Kconfig or CDL files used in various systems software.
For Kconfig, you need our modified configurator (protconf-amd64) from https://code.google.com/p/linux-variability-analysis-tools/source/browse/?repo=exconfig in order to export a Kconfig model into our own format (based on Google ProtocolBuffers). For an overview of projects that use the Kconfig infrastructure (the configurator and Kconfig files specifying the configuration options) see for instance:
Thorsten Berger, Steven She, Rafael Lotufo, Andrzej Wasowski, Krzysztof Czarnecki, "A Study of Variability Models and Languages in the Systems Software Domain," IEEE Transactions on Software Engineering, Volume 39, Issue 12. 2013 (also available as a technical report)
Run the conversion with
sbt run-main gsd.vm.VM2DimacsMain <input file> <output.dimacs>
whereas <input file> refers to a model file in .sxfm (SPLOT model), .pb or .exconfig (Kconfig model) or .iml (CDL model).
- Thorsten Berger email@example.com
VM2BOOL further relies on