Diagnosis

[manleviet]

Major changes in this pull request are:

1. A new package called diagnosis, situated inside the operations package, stores classes related to diagnosis tasks. This package includes implementations of FastDiag, QuickXPlain, and HSDAG. Besides, the DiagnosisModel class is responsible for preparing sets of constraints for diagnosis tasks, while the ConsistencyChecker class serves as a solver wrapper that checks the validity of assumptions with the background knowledge.
2. I added two operations called Glucose3Diagnosis and Glucose3Conflict that use HSDAG and FastDiag/QuickXPlain to identify all diagnoses/conflicts.
3. The only change in PySATModel is a new map of <name of relationship/constraint, clauses>. This map helps to create pretty diagnosis messages.
4. I created DiagnosisModel, which gets a PySATModel object as input and does two things:
   1. Add a reify variable for each clause. All new clauses will be added to the solver as background knowledge.
   2. Put reify variables into two sets, C - the consideration set -, and B - the correct constraints. C and B will be translated into assumptions to be checked.
      The advantage of this approach is that the solver is only created once, and consistency checks don’t have too much overhead. This is particularly useful for complex feature models.
5. DiagnosisModel supports four diagnosis tasks:
   1. Feature model diagnosis: C = CF, B = {f0=true}
   2. Configuration diagnosis: C = configuration constraints, B = CF + {f0=true}
   3. Feature model debugging: C = CF, B = {f0=true} + test_case
   4. Redundancy detection task: C = CF, B = {}

An issue:
Glucose3Diagnosis and Glucose3Conflict implement the following functions: (1) set_configuration, (2) set_test_case. These functions are not mandatory in every case. For example, set_configuration is used when we want to diagnose for an inconsistent configuration. Thus, Glucose3Diagnosis and Glucose3Conflict currently implement Operation, not ErrorDiagnosis or ValidConfiguration. In other words, we cannot use them via the command line with DiscoverMetamodels. Is it possible to have a new operation that allows for optional set_configuration and optional set_test_case?

[jagalindo]

@manleviet I've been taking a look at the pr. There are some issues with the solution you proposed to use. The main is that you add a new Model, which should not be used as it would break compatibility with other plugins.

I'm creating a new empty operation so you can implement/adapt the implementation you made.

[jagalindo]

@manleviet I'm taking a look to the PR. Could you explain why you need two relationships for the mandatory:

<<<<<<< diagnosis
clause_1 = [
-1 *
self.destination_model.variables.get(relation.parent.name),
self.destination_model.variables.get(relation.children[0].name)
]
clause_2 = [
-1 *
self.destination_model.variables.get(
relation.children[0].name),
self.destination_model.variables.get(relation.parent.name)
]
self.destination_model.add_clause(clause_1)
self.destination_model.add_clause(clause_2)
self.destination_model.add_clause_toMap(str(relation), [clause_1, clause_2])

    elif relation.is_optional():
        clause = [
            -1 *
            self.destination_model.variables.get(
                relation.children[0].name),
            self.destination_model.variables.get(relation.parent.name)
        ]
        self.destination_model.add_clause(clause)
        self.destination_model.add_clause_toMap(str(relation), [clause])

=======
self.destination_model.add_clause([-1 * value_parent, value_children])
self.destination_model.add_clause([-1 * value_children, value_parent])

    elif relation.is_optional():
        self.destination_model.add_clause([-1 * value_children, value_parent])

develop

    elif relation.is_or():  # this is a 1 to n relatinship with multiple childs
        clauses = []
        # add the first cnf child1 or child2 or ... or childN or no parent)
        # first elem of the constraint
        alt_cnf = [-1 * value_parent]
        for child in relation.children:

<<<<<<< diagnosis
alt_cnf.append(
self.destination_model.variables.get(child.name))
clauses.append(alt_cnf)
# self.destination_model.add_clause(alt_cnf)

        for child in relation.children:
            clauses.append([
                -1 * self.destination_model.variables.get(child.name),
                self.destination_model.variables.get(relation.parent.name)

=======
alt_cnf.append(self.destination_model.get_variable(child.name))
self.destination_model.add_clause(alt_cnf)

        for child in relation.children:
            self.destination_model.add_clause([
                -1 * self.destination_model.get_variable(child.name),
                value_parent

develop

[jagalindo]

I don't understand why you have to modify the fm-to-pysat transformation

[jagalindo]

Ok, It looks like all those changes only seek to store the clauses in a map. This could have been easily solved by adding that in the pysat metamodel class. Also, why not relying on the cnf() class of pysat to access that data?

[jagalindo]

@manleviet I'm pushing a new version to your repo, so we can merge when ready. Give me a few days to finish it

[manleviet]

Hello @jagalindo ,

I'm sorry for not getting back to you sooner. I'm currently on vacation in Vietnam.

1. I made changes in fm_to_pysat.py according to your proposal. ;-)

2. I need a map that links relationships/constraints to clauses, to generate clear and concise diagnosis messages. Without this map, the diagnosis message could be confusing, e.g., "[-1, 2]" or "[-2, 1]" - containing only one of two clauses corresponding to "mandatory(1, 2)". So if we have the map, the diagnosis message will be more intuitive and understandable, e.g., [mandatory(1, 2)].

This is also why changes were made in fm_to_pysat.py, not in cnf_to_pysat.py, as CNF provides no information about relationships/constraints.

3. DiagnosisModel is separated from PySATModel and is required by only diagnosis operations. So it may face an issue only if other plugins require the diagnosis operations.

I'm fine with your new version. Please inform me when you are done.

[jagalindo]

@manleviet Please verify that I didnt break anything with the changes. Also, please, adhere to the prospector and mypi conventions so we can merge the PR.

Regards

[jagalindo]

Ok, we need to merge this asap To keep on going with dev changes. I'll merge with the mypi problems and then ask for help to correct them