VM2BOOL converts feature models (SPLOT SXFM, Linux Kconfig, eCos CDL) into propositional formulas (DIMACS).

You can obtain SPLOT feature models from or Kconfig and CDL models from . 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 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)

Running VM2BOOL

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).


VM2BOOL further relies on