Plugins
The flamapy framework is designed to support automated analysis of feature models through a modular and extensible architecture. This flexibility is primarily achieved through the use of plugins, each encapsulating specific functionality, metamodels, and operations.
Table of contents
Concept of plugins
Plugins in flamapy are the fundamental building blocks that extend the framework’s capabilities. Each plugin is designed to handle a specific type of analysis or transformation related to feature models. The plugins encapsulate:
Metamodel classes
Define the structure and constraints of the variability models.
Operations
Implement the actual analyses or computations that can be performed on the models.
Transformations
Handle the conversion between different model representations, crucial for leveraging various computational techniques.
Architecture overview
Core plugin
The core plugin provides the foundational elements of the framework, including interfaces for different transformations (Text-to-Model, Model-to-Text, Model-to-Model), and mechanisms for identifying and executing available operations.
Metamodel plugins
These plugins define the specific variability models and their associated operations and transformations. Examples include the feature model plugin, PySAT plugin, and BDD plugin.
Available plugins
flamapy offers a variety of plugins, each tailored to specific analysis needs and model types. Here are some of the key plugins available. Each plugin is provided in the Pypi package manager:
flamapy_fw
This is the main repository hosting the core components of flamapy . It includes the essential infrastructure for the framework, enabling plugin management, and execution of operations and transformations. Github
fm_metamodel
Hosts the concrete classes for feature models. It supports multiple feature model formats and provides various operations such as counting leaf features, estimating the number of valid configurations, and identifying core features. Github
pysat_metamodel
Provides the integration with PySAT, a meta-solver that enables the analysis of feature models using various SAT solvers. This plugin is essential for performing constraint satisfaction problems and other complex analyses. Github
bdd_metamodel
Supports Binary Decision Diagrams (BDDs) for the automated analysis of feature models. This plugin is particularly useful for operations that benefit from BDD techniques, such as counting valid configurations efficiently. Github
z3_metamodel
Integrates the Z3 SMT solver to enable analysis of feature models with typed attributes (Integer, Real, String). Supports satisfiability checking, configuration enumeration, attribute bound computation, and attribute optimization beyond Boolean logic. Github
pysat_diagnosis_metamodel
Extends the PySAT plugin with diagnosis capabilities. Given a configuration and a test case, it computes conflict sets (minimal inconsistent subsets of constraints) and diagnoses (minimal corrections). Built on the QuickXPlain and FastDiag algorithms. Github
sharpsat_metamodel
Provides scalable approximate model counting and almost-uniform sampling of configurations. It reuses the SAT CNF and relies on ApproxMC (pyapproxmc) and UniGen (pyunigen), scaling beyond the exact enumeration of the SAT/Z3 backends and the memory-bound BDD backend. Github
sdd_metamodel
Compiles a feature model into a Sentential Decision Diagram (SDD) for exact analysis (configurations number, satisfiable, core and dead features). SDDs are more succinct than OBDDs in some cases and are built on top of the SAT CNF with PySDD. Optional extra flamapy[sdd]; see the community plugins page. Github
dnnf_metamodel
Exact analysis via d-DNNF knowledge compilation (configurations number, satisfiable) that scales to large industrial models. It relies on the d4 compiler, a native binary that must be installed separately (it has no PyPI package) and exposed as d4 on PATH or via FLAMAPY_D4_PATH. Optional extra flamapy[dnnf]; see the community plugins page. Github