Pizza FM with full expressiveness for SMT analysis
Description
This feature model presents a comprehensive pizza Software Product Line (SPL) designed to showcase the full expressiveness of UVL. It is specifically structured for analysis using SMT solvers (such as Z3).
The model contains 15 features in total, including 2 typed features (Integer, String) and 2 feature attributes (Price, Kcal); and 7 cross-tree constraints combining propositional, arithmetic, and aggregation logic over typed features and attributes. The model has 105 satisfiable configurations (228 when considering only the Boolean projection); 6 core features (SpicyLvl, Pizza, Topping, Size, Normal, Dough), 2 dead features (Name, Big), and 2 false-optional features (SpicyLvl, Normal).
Dataset fact label
What the fact labels of its 1 models say together.
| Models | 1 | |||
|---|---|---|---|---|
| Analysed | 1 | |||
| UVL language | ||||
| Boolean | 1 | |||
| Arithmetic | 1 | |||
| Arithmetic, aggregate functions | 1 | |||
| Type | 1 | |||
| Size and structure | Least | Median | Most | Total |
|---|---|---|---|---|
| Features | 15 | 15 | 15 | 15 |
| Leaf features | 11 | 11 | 11 | 11 |
| Cross-tree constraints | 7 | 7 | 7 | 7 |
| Depth of the tree | 2 | 2 | 2 | |
| Groups | 3 | 3 | 3 | 3 |
| Analysis | |
|---|---|
| Satisfiable | 1 / 1 |
| With dead features | 0 |
| With false optional features | 0 |
| Configurations | 228 |
| Variability | |
| Total variability | 0.7 % |
| Homogeneity | 62.2 % |
