FmToBDD from propositional formula

flamapy/metamodels/bdd_metamodel/models/bdd_model.py

@@ -33,7 +33,7 @@ def __init__(self) -> None:
         self.variables: dict[str, int] = {}
 
     @classmethod
-    def from_textual_cnf(cls, cnf_formula: str, variables: list[str]) -> 'BDDModel':
+    def from_cnf_formula(cls, cnf_formula: str, variables: list[str]) -> 'BDDModel':
         """Build the BDD from a textual representation of the CNF formula,
         and the list of variables."""
         bdd_model = cls()
@@ -46,6 +46,20 @@ def from_textual_cnf(cls, cnf_formula: str, variables: list[str]) -> 'BDDModel':
         bdd_model.variables = bdd_model.bdd.vars
         return bdd_model
 
+    @classmethod
+    def from_propositional_formula(cls, formula: str, variables: list[str]) -> 'BDDModel':
+        """Build the BDD from a textual representation of the CNF formula,
+        and the list of variables."""
+        bdd_model = cls()
+        # Declare variables
+        for var in variables:
+            bdd_model.bdd.declare(var)
+        # Build the BDD
+        bdd_model.root = bdd_model.bdd.add_expr(formula)
+        # Store variables
+        bdd_model.variables = bdd_model.bdd.vars
+        return bdd_model
+
     def nof_nodes(self) -> int:
         """Return number of nodes in the BDD."""
         return len(self.bdd)

flamapy/metamodels/bdd_metamodel/transformations/__init__.py

@@ -1,4 +1,4 @@
-from .fm_to_bdd import FmToBDD
+from .fm_to_bdd_pl import FmToBDD
 from .json_writer import JSONWriter
 from .json_reader import JSONReader
 from .pickle_writer import PickleWriter

flamapy/metamodels/bdd_metamodel/transformations/fm_to_bdd_cnf.py

@@ -0,0 +1,202 @@
+import itertools
+from typing import Optional, Any
+
+from flamapy.core.transformations import ModelToModel
+from flamapy.metamodels.fm_metamodel.models import (
+    FeatureModel,
+    Constraint,
+    Feature,
+    Relation,
+)
+from flamapy.metamodels.bdd_metamodel.models import BDDModel
+
+
+class FmToBDD(ModelToModel):
+
+    @staticmethod
+    def get_source_extension() -> str:
+        return "fm"
+
+    @staticmethod
+    def get_destination_extension() -> str:
+        return "bdd"
+
+    def __init__(self, source_model: FeatureModel) -> None:
+        self.source_model = source_model
+        self.counter = 1
+        self.destination_model: Optional[BDDModel] = None
+        self.variables: dict[str, int] = {}
+        self.features: dict[int, str] = {}
+        self.clauses: list[list[int]] = []
+
+    def _get_variable(self, name: str) -> int:
+        variable = self.variables.get(name)
+        if variable is None:
+            raise ValueError("the parent variable wasn't found")
+        return variable
+
+    def add_feature(self, feature: Feature) -> None:
+        if feature.name not in self.variables:
+            self.variables[feature.name] = self.counter
+            self.features[self.counter] = feature.name
+            self.counter += 1
+
+    def add_root(self, feature: Feature) -> None:
+        self.clauses.append([self._get_variable(feature.name)])
+
+    def _add_mandatory_relation(self, relation: Relation) -> list[list[int]]:
+        value_parent = self._get_variable(relation.parent.name)
+        value_child = self._get_variable(relation.children[0].name)
+        clauses = [[-1 * value_parent, value_child], [-1 * value_child, value_parent]]
+        return clauses
+
+    def _add_optional_relation(self, relation: Relation) -> list[list[int]]:
+        value_parent = self._get_variable(relation.parent.name)
+        value_children = self._get_variable(relation.children[0].name)
+        clauses = [[-1 * value_children, value_parent]]
+        return clauses
+
+    def _add_or_relation(self, relation: Relation) -> list[list[int]]:
+        # this is a 1 to n relatinship with multiple childs
+        # add the first cnf child1 or child2 or ... or childN or no parent)
+        # first elem of the constraint
+        value_parent = self._get_variable(relation.parent.name)
+
+        alt_cnf = [-1 * value_parent]
+        for child in relation.children:
+            alt_cnf.append(self._get_variable(child.name))
+        clauses = [alt_cnf]
+
+        for child in relation.children:
+            clauses.append([
+                -1 * self._get_variable(child.name),
+                value_parent
+            ])
+
+        return clauses
+
+    def _add_alternative_relation(self, relation: Relation) -> list[list[int]]:
+        # this is a 1 to 1 relatinship with multiple childs
+        # add the first cnf child1 or child2 or ... or childN or no parent)
+
+        value_parent = self._get_variable(relation.parent.name)
+        # first elem of the constraint
+        alt_cnf = [-1 * value_parent]
+        for child in relation.children:
+            alt_cnf.append(self._get_variable(child.name))
+        clauses = [alt_cnf]
+
+        for i, _ in enumerate(relation.children):
+            for j in range(i + 1, len(relation.children)):
+                if i != j:
+                    clauses.append([
+                        -1 * self._get_variable(relation.children[i].name),
+                        -1 * self._get_variable(relation.children[j].name)
+                    ])
+            clauses.append([
+                -1 * self._get_variable(relation.children[i].name),
+                value_parent
+            ])
+        return clauses
+
+    def _add_constraint_relation(self, relation: Relation) -> list[list[int]]:
+        value_parent = self._get_variable(relation.parent.name)
+
+        # This is a _min to _max relationship
+        _min = relation.card_min
+        _max = relation.card_max
+
+        clauses = []
+
+        for val in range(len(relation.children) + 1):
+            if val < _min or val > _max:
+                # combinations of val elements
+                for combination in itertools.combinations(relation.children, val):
+                    cnf = [-1 * value_parent]
+                    for feat in relation.children:
+                        if feat in combination:
+                            cnf.append(-1 * self._get_variable(feat.name))
+                        else:
+                            cnf.append(self._get_variable(feat.name))
+                    clauses.append(cnf)
+
+        # there is a special case when coping with the upper part of the thru table
+        # In the case of allowing 0 childs, you cannot exclude the option  in that
+        # no feature in this relation is activated
+        for val in range(1, len(relation.children) + 1):
+
+            for combination in itertools.combinations(relation.children, val):
+                cnf = [value_parent]
+                for feat in relation.children:
+                    if feat in combination:
+                        cnf.append(-1 * self._get_variable(feat.name))
+                    else:
+                        cnf.append(self._get_variable(feat.name))
+                clauses.append(cnf)
+        return clauses
+
+    def add_relation(self, relation: Relation) -> None:
+        if relation.is_mandatory():
+            clauses = self._add_mandatory_relation(relation)
+        elif relation.is_optional():
+            clauses = self._add_optional_relation(relation)
+        elif relation.is_or():  
+            clauses = self._add_or_relation(relation)
+        elif relation.is_alternative():  
+            clauses = self._add_alternative_relation(relation)
+        else:
+            clauses = self._add_constraint_relation(relation)
+        self._store_constraint_clauses(clauses)
+
+    def _store_constraint_clauses(self, clauses: list[list[int]]) -> None:
+        for clause in clauses:
+            self.clauses.append(clause)
+
+    def add_constraint(self, ctc: Constraint) -> None:
+        def get_term_variable(term: Any) -> int:
+            if term.startswith('-'):
+                return -self._get_variable(term[1:])
+
+            return self._get_variable(term)
+
+        clauses = ctc.ast.get_clauses()
+        for clause in clauses:
+            clause_variables = list(map(get_term_variable, clause))
+            self.clauses.append(clause_variables)
+
+    def transform(self) -> BDDModel:
+        for feature in self.source_model.get_features():
+            self.add_feature(feature)
+
+        self.add_root(self.source_model.root)
+
+        for relation in self.source_model.get_relations():
+            self.add_relation(relation)
+
+        for constraint in self.source_model.get_constraints():
+            self.add_constraint(constraint)
+
+        # Transform clauses to textual CNF notation required by the BDD
+        not_connective = BDDModel.NOT
+        or_connective = " " + BDDModel.OR + " "
+        and_connective = " " + BDDModel.AND + " "
+        cnf_list = []
+        for clause in self.clauses:
+            cnf_list.append(
+                "("
+                + or_connective.join(
+                    list(
+                        map(
+                            lambda elem: not_connective + self.features[abs(elem)]
+                            if elem < 0
+                            else self.features[abs(elem)],
+                            clause,
+                        )
+                    )
+                )
+                + ")"
+            )
+        cnf_formula = and_connective.join(cnf_list)
+        self.destination_model = BDDModel.from_cnf_formula(cnf_formula, 
+                                                           list(self.variables.keys()))
+        return self.destination_model

flamapy/metamodels/bdd_metamodel/transformations/fm_to_bdd_pl.py

@@ -0,0 +1,124 @@
+import re
+from typing import Optional
+
+from flamapy.core.models.ast import ASTOperation
+from flamapy.core.transformations import ModelToModel
+from flamapy.metamodels.fm_metamodel.models import FeatureModel, Relation
+from flamapy.metamodels.bdd_metamodel.models import BDDModel
+
+
+class FmToBDD(ModelToModel):
+
+    @staticmethod
+    def get_source_extension() -> str:
+        return "fm"
+
+    @staticmethod
+    def get_destination_extension() -> str:
+        return "bdd"
+
+    def __init__(self, source_model: FeatureModel) -> None:
+        self.source_model = source_model
+        self.destination_model: Optional[BDDModel] = None
+
+    def transform(self) -> BDDModel:
+        formula, variables = traverse_feature_tree(self.source_model)
+        self.destination_model = BDDModel.from_propositional_formula(formula, variables)
+        return self.destination_model
+
+
+def traverse_feature_tree(feature_model: FeatureModel) -> tuple[str, list[str]]:
+    """Traverse the feature tree from the root and return the propositional formula and 
+    the list of variables (features's names).
+    """
+    if feature_model is None or feature_model.root is None:
+        return ('', [])
+    formula = [feature_model.root.name]  # The root is always present
+    variables = []
+    for feature in feature_model.get_features():
+        variables.append(feature.name)
+        for relation in feature.get_relations():
+            if relation.is_mandatory():
+                formula.append(get_mandatory_formula(relation))
+            elif relation.is_optional():
+                formula.append(get_optional_formula(relation))
+            elif relation.is_or():
+                formula.append(get_or_formula(relation))
+            elif relation.is_alternative():
+                formula.append(get_alternative_formula(relation))
+            elif relation.is_mutex():
+                formula.append(get_mutex_formula(relation))
+            elif relation.is_cardinal():
+                formula.append(get_cardinality_formula(relation))
+    for constraint in feature_model.get_constraints():
+        ctc = str(
+            re.sub(rf"\b{ASTOperation.EXCLUDES.value}\b", 
+                   "=> !",
+                   re.sub(rf"\b{ASTOperation.REQUIRES.value}\b", 
+                          "=>",
+                          re.sub(rf"\b{ASTOperation.EQUIVALENCE.value}\b", 
+                                 "<=>",
+                                 re.sub(rf"\b{ASTOperation.IMPLIES.value}\b", 
+                                        "=>",
+                                        re.sub(rf"\b{ASTOperation.OR.value}\b", 
+                                               "|",
+                                               re.sub(rf"\b{ASTOperation.AND.value}\b", 
+                                                      "&",
+                                                      re.sub(rf"\b{ASTOperation.NOT.value}\b", 
+                                                             "!",
+                                                             constraint.ast.pretty_str()))))))))
+        formula.append(ctc)
+    propositional_formula = ' & '.join(f'({f})' for f in formula)
+    return (propositional_formula, variables)
+
+
+def get_mandatory_formula(relation: Relation) -> str:
+    return f'{relation.parent.name} <=> {relation.children[0].name}'
+
+
+def get_optional_formula(relation: Relation) -> str:
+    return f'{relation.children[0].name} => {relation.parent.name}'
+
+
+def get_or_formula(relation: Relation) -> str:
+    return f'{relation.parent.name} <=> ({" | ".join(child.name for child in relation.children)})'
+
+
+def get_alternative_formula(relation: Relation) -> str:
+    formula = []
+    for child in relation.children:
+        children_negatives = set(relation.children) - {child}
+        formula.append(f'{child.name} <=> '
+                       f'({" & ".join("!" + f.name for f in children_negatives)} '
+                       f'& {relation.parent.name})')
+    return " & ".join(f'({f})' for f in formula)
+
+
+def get_mutex_formula(relation: Relation) -> str:
+    formula = []
+    for child in relation.children:
+        children_negatives = set(relation.children) - {child}
+        formula.append(f'{child.name} <=> '
+                       f'({" & ".join("!" + f.name for f in children_negatives)} '
+                       f'& {relation.parent.name})')
+    formula_str = " & ".join(f'({f})' for f in formula)
+    return f'({relation.parent.name} <=> !({" | ".join(child.name for child in relation.children)})) ' \
+           f'| ({formula_str})'
+
+
+def get_cardinality_formula(relation: Relation) -> str:
+    children = [child.name for child in relation.children]
+    or_ctc = []
+    for k in range(relation.card_min, relation.card_max + 1):
+        combi_k = list(itertools.combinations(children, k))
+        for positives in combi_k:
+            negatives = children - set(positives)
+            positives_and_ctc = f'{" & ".join(positives)}'
+            negatives_and_ctc = f'{" & ".join("!" + f for f in negatives)}'
+            if positives_and_ctc and negatives_and_ctc:
+                and_ctc = f'{positives_and_ctc} & {negatives_and_ctc}'
+            else:
+                and_ctc = f'{positives_and_ctc}{negatives_and_ctc}'
+            or_ctc.append(and_ctc) 
+    formula_or_ctc = f'{" | ".join(or_ctc)}'
+    return f'{relation.parent.name} <=> {formula_or_ctc}'