Add FeatureModelAnomaly implementation

build.gradle

@@ -16,6 +16,7 @@ dependencies {
     implementation 'org.springframework.boot:spring-boot-starter-web'
     implementation 'org.springframework.boot:spring-boot-starter-validation'
     implementation 'com.bpodgursky:jbool_expressions:1.24'
+    implementation files('lib/de.ovgu.featureide.lib.fm-v3.9.1.jar', 'lib/uvl-parser.jar')
     testImplementation 'org.springframework.boot:spring-boot-starter-test'
 }
 

src/main/java/edu/kit/provideq/toolbox/exception/ConversionException.java

@@ -0,0 +1,10 @@
+package edu.kit.provideq.toolbox.exception;
+
+public class ConversionException extends Exception {
+    public ConversionException(String message) {
+        super(message);
+    }
+    public ConversionException(String message, Throwable cause) {
+        super(message, cause);
+    }
+}

src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/FeatureModelAnomalyController.java

@@ -0,0 +1,49 @@
+package edu.kit.provideq.toolbox.featureModel.anomaly;
+
+import edu.kit.provideq.toolbox.ProblemController;
+import edu.kit.provideq.toolbox.ProblemSolverInfo;
+import edu.kit.provideq.toolbox.SolutionHandle;
+import edu.kit.provideq.toolbox.featureModel.anomaly.solvers.*;
+import edu.kit.provideq.toolbox.meta.MetaSolver;
+import edu.kit.provideq.toolbox.meta.ProblemType;
+import org.springframework.web.bind.annotation.*;
+
+import javax.validation.Valid;
+import java.util.Set;
+
+@RestController
+public class FeatureModelAnomalyController extends ProblemController<String, String, FeatureModelAnomalySolver> {
+
+  private final MetaSolver<FeatureModelAnomalySolver> metaSolver;
+
+  public FeatureModelAnomalyController(MetaSolver<FeatureModelAnomalySolver> metaSolver) {
+    this.metaSolver = metaSolver;
+  }
+
+  @Override
+  public ProblemType getProblemType() {
+    return ProblemType.FEATURE_MODEL_ANOMALY;
+  }
+
+  @Override
+  public MetaSolver<FeatureModelAnomalySolver> getMetaSolver() {
+    return metaSolver;
+  }
+
+  @CrossOrigin
+  @PostMapping("/solve/featureModel/anomaly")
+  public SolutionHandle solve(@RequestBody @Valid SolveFeatureModelAnomalyRequest request) {
+    return super.solve(request);
+  }
+
+  @GetMapping("/solve/featureModel/anomaly")
+  public SolutionHandle getSolution(@RequestParam(name = "id", required = true) long id) {
+    return super.getSolution(id);
+  }
+
+  @CrossOrigin
+  @GetMapping("/solvers/featureModel/anomaly")
+  public Set<ProblemSolverInfo> getSolvers() {
+    return super.getSolvers();
+  }
+}

src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/MetaSolverFeatureModelAnomaly.java

@@ -0,0 +1,28 @@
+package edu.kit.provideq.toolbox.featureModel.anomaly;
+
+import edu.kit.provideq.toolbox.meta.MetaSolver;
+import edu.kit.provideq.toolbox.meta.Problem;
+import org.springframework.beans.factory.annotation.Autowired;
+import edu.kit.provideq.toolbox.featureModel.anomaly.solvers.*;
+import org.springframework.stereotype.Component;
+
+import java.util.ArrayList;
+import java.util.Random;
+
+/**
+ * Simple {@link MetaSolver} for FeatureModel problems
+ */
+@Component
+public class MetaSolverFeatureModelAnomaly extends MetaSolver<FeatureModelAnomalySolver> {
+
+  @Autowired
+  public MetaSolverFeatureModelAnomaly(FeatureModelAnomalySolver anomalySolver) {
+    super(anomalySolver);
+  }
+
+  @Override
+  public FeatureModelAnomalySolver findSolver(Problem problem) {
+    // todo add decision
+    return (new ArrayList<>(this.solvers)).get((new Random()).nextInt(this.solvers.size()));
+  }
+}

src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/SolveFeatureModelAnomalyRequest.java

@@ -0,0 +1,9 @@
+package edu.kit.provideq.toolbox.featureModel.anomaly;
+
+import edu.kit.provideq.toolbox.SolveRequest;
+
+/**
+ * POST Requests to /solve/featureModel should have a response body of this form.
+ * The needed formula the featureModel formula to solve in the DIMACS CNF - SAT format.
+ */
+public class SolveFeatureModelAnomalyRequest extends SolveRequest<String> {}

src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/solvers/FeatureModelAnomalySolver.java

@@ -0,0 +1,70 @@
+package edu.kit.provideq.toolbox.featureModel.anomaly.solvers;
+
+import edu.kit.provideq.toolbox.Solution;
+import edu.kit.provideq.toolbox.SolutionStatus;
+import edu.kit.provideq.toolbox.exception.ConversionException;
+import edu.kit.provideq.toolbox.featureModel.convert.UvlToDimacsCNF;
+import edu.kit.provideq.toolbox.meta.Problem;
+import edu.kit.provideq.toolbox.meta.ProblemType;
+import edu.kit.provideq.toolbox.sat.solvers.GamsSATSolver;
+import edu.kit.provideq.toolbox.sat.solvers.SATSolver;
+import org.springframework.beans.factory.annotation.Autowired;
+import org.springframework.stereotype.Component;
+
+@Component
+public class FeatureModelAnomalySolver extends FeatureModelSolver {
+    private final SATSolver satSolver;
+
+    @Autowired
+    public FeatureModelAnomalySolver(
+            GamsSATSolver satSolver) {
+        this.satSolver = satSolver;
+    }
+
+    @Override
+    public String getName() {
+        return "Feature Model Anomaly via GAMS SAT";
+    }
+
+    @Override
+    public boolean canSolve(Problem<String> problem) {
+        //TODO: assess problemData
+        return problem.type() == ProblemType.MAX_CUT;
+    }
+
+    @Override
+    public float getSuitability(Problem<String> problem) {
+        //TODO: implement algorithm for suitability calculation
+        return 1;
+    }
+
+    @Override
+    public void solve(Problem<String> problem, Solution<String> solution) {
+        // Convert uvl to cnf
+        String cnf;
+        try {
+            cnf = UvlToDimacsCNF.convert(problem.problemData());
+        } catch (ConversionException e) {
+            solution.setDebugData("Conversion error: " + e.getMessage());
+            return;
+        }
+
+        // todo Add a real solution collection which handles part solutions and still saves solvers and meta data for each
+        var solutionBuilder = new StringBuilder();
+
+        // Check if the FM is a Void Feature Model
+        var voidSolution = new Solution<String>(-1);
+        satSolver.solve(new Problem<>(cnf, ProblemType.SAT), voidSolution);
+        if (voidSolution.getStatus() == SolutionStatus.SOLVED) {
+            solutionBuilder.append(voidSolution.getSolutionData());
+        } else {
+            solutionBuilder.append(voidSolution.getDebugData());
+        }
+
+        // Check if there are any Dead Features
+        var deadSolution = new Solution<String>(-1);
+        satSolver.solve(new Problem<>(cnf, ProblemType.SAT), deadSolution);
+
+        solution.setSolutionData(solutionBuilder.toString());
+    }
+}

src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/solvers/FeatureModelSolver.java

@@ -0,0 +1,6 @@
+package edu.kit.provideq.toolbox.featureModel.anomaly.solvers;
+
+import edu.kit.provideq.toolbox.meta.ProblemSolver;
+
+public abstract class FeatureModelSolver implements ProblemSolver<String, String> {
+}

src/main/java/edu/kit/provideq/toolbox/featureModel/convert/UvlToDimacsCNF.java

@@ -0,0 +1,51 @@
+package edu.kit.provideq.toolbox.featureModel.convert;
+
+import de.ovgu.featureide.fm.core.analysis.cnf.formula.FeatureModelFormula;
+import de.ovgu.featureide.fm.core.base.IFeatureModel;
+import de.ovgu.featureide.fm.core.base.impl.MultiFeatureModel;
+import de.ovgu.featureide.fm.core.init.FMCoreLibrary;
+import de.ovgu.featureide.fm.core.io.FormatHandler;
+import de.ovgu.featureide.fm.core.io.Problem;
+import de.ovgu.featureide.fm.core.io.dimacs.DIMACSFormatCNF;
+import de.ovgu.featureide.fm.core.io.uvl.UVLFeatureModelFormat;
+import edu.kit.provideq.toolbox.exception.ConversionException;
+
+import java.util.List;
+import java.util.stream.Collectors;
+
+public class UvlToDimacsCNF {
+    static {
+        FMCoreLibrary.getInstance().install();
+    }
+
+    public static String convert(String content) throws ConversionException {
+        CharSequence charSequence = content.subSequence(0, content.length());
+
+        // Init empty model
+        var model = new MultiFeatureModel("de.ovgu.featureide.fm.core.MultiFeatureModelFactory");
+
+        // Parse uvl
+        var uvlFeatureModelHandler = new FormatHandler<>(new UVLFeatureModelFormat(), model);
+        List<Problem> problems = uvlFeatureModelHandler.read(charSequence);
+        if (problems.size() > 0) {
+            throw new ConversionException("UVL conversion resulted in errors "
+                    + problems
+                    .stream()
+                    .map(Object::toString)
+                    .collect(Collectors.joining("\n")));
+        }
+
+        IFeatureModel fm = uvlFeatureModelHandler.getObject();
+
+        FeatureModelFormula featureModelFormula = new FeatureModelFormula(fm);
+        var cnf = featureModelFormula.getCNF();
+
+//        TseitinConverter tseitinConverter = new TseitinConverter();
+//        var nodes = new ArrayList<Node>();
+//        nodes.add(featureModelFormula.getCNFNode());
+//        var convertedFM = tseitinConverter.convert(fm, nodes, false);
+//        System.out.println(new DIMACSFormatCNF().write(new FeatureModelFormula(convertedFM).getCNF()));
+
+        return new DIMACSFormatCNF().write(cnf);
+    }
+}

src/main/java/edu/kit/provideq/toolbox/meta/ProblemType.java

@@ -14,5 +14,12 @@ public enum ProblemType {
    * An optimization problem:
    * For a given graph, find the optimal separation of vertices that maximises the cut crossing edge weight sum.
    */
-  MAX_CUT
+  MAX_CUT,
+
+  /**
+   * A searching problem:
+   * For a given feature model, check for Void Feature Model & Dead Features.
+   * <a href="https://sdq.kastel.kit.edu/publications/pdfs/kowal2016b.pdf">More information</a>
+   */
+  FEATURE_MODEL_ANOMALY,
 }

src/main/java/edu/kit/provideq/toolbox/sat/convert/BoolExprToDimacsCNF.java

@@ -15,6 +15,8 @@ public final class BoolExprToDimacsCNF {
     private final static String negationPrefix = "-";
 
     public static String convert(String boolExpr) {
+        if (boolExpr.contains("p cnf")) return boolExpr;
+
         // Streamline bool expr format
         boolExpr = boolExpr
                 .replaceAll("\\b(?:not|NOT)\\b", "!")

src/test/java/edu/kit/provideq/toolbox/featureModel/UvlToDimacsCNFTests.java

@@ -0,0 +1,95 @@
+package edu.kit.provideq.toolbox.featureModel;
+
+import edu.kit.provideq.toolbox.exception.ConversionException;
+import edu.kit.provideq.toolbox.featureModel.convert.UvlToDimacsCNF;
+import org.junit.jupiter.api.Test;
+import org.springframework.boot.test.context.SpringBootTest;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+@SpringBootTest
+public class UvlToDimacsCNFTests {
+    @Test
+    public void TestSimple() throws ConversionException {
+        String converted = UvlToDimacsCNF.convert("""   
+                features
+                	Sandwich {extended__}
+                		mandatory
+                			Bread
+                				alternative
+                					"Full Grain" {Calories 203, Price 1.99, Organic true}
+                					Flatbread {Calories 90, Price 0.79, Organic true}
+                					Toast {Calories 250, Price 0.99, Organic false}
+                		optional
+                			Cheese
+                				optional
+                					Gouda
+                						alternative
+                							Sprinkled {Fat {value 35, unit "g"}}
+                							Slice {Fat {value 35, unit "g"}}
+                					Cheddar
+                					"Cream Cheese"
+                			Meat
+                				or
+                					"Salami" {Producer "Farmer Bob"}
+                					Ham {Producer "Farmer Sam"}
+                					"Chicken Breast" {Producer "Farmer Sam"}
+                			Vegetables
+                				optional
+                					"Cucumber"
+                					Tomatoes
+                					Lettuce
+                """);
+
+        assertEquals(converted.replace("\r\n", "\n"), ("""
+                c 1 Sandwich
+                c 2 Bread
+                c 3 Full Grain
+                c 4 Flatbread
+                c 5 Toast
+                c 6 Cheese
+                c 7 Gouda
+                c 8 Sprinkled
+                c 9 Slice
+                c 10 Cheddar
+                c 11 Cream Cheese
+                c 12 Meat
+                c 13 Salami
+                c 14 Ham
+                c 15 Chicken Breast
+                c 16 Vegetables
+                c 17 Cucumber
+                c 18 Tomatoes
+                c 19 Lettuce
+                p cnf 19 27
+                1 0
+                1 -2 0
+                1 -6 0
+                1 -12 0
+                1 -16 0
+                2 -1 0
+                2 -3 0
+                2 -4 0
+                2 -5 0
+                3 4 5 -2 0
+                -3 -4 0
+                -3 -5 0
+                -4 -5 0
+                6 -7 0
+                6 -10 0
+                6 -11 0
+                7 -8 0
+                7 -9 0
+                8 9 -7 0
+                -8 -9 0
+                12 -13 0
+                12 -14 0
+                12 -15 0
+                13 14 15 -12 0
+                16 -17 0
+                16 -18 0
+                16 -19 0
+                """)
+        );
+    }
+}