diff --git a/build.gradle b/build.gradle index a7a2723f..93affcd5 100644 --- a/build.gradle +++ b/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' } diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar index 249e5832..41d9927a 100644 Binary files a/gradle/wrapper/gradle-wrapper.jar and b/gradle/wrapper/gradle-wrapper.jar differ diff --git a/lib/de.ovgu.featureide.lib.fm-v3.9.1.jar b/lib/de.ovgu.featureide.lib.fm-v3.9.1.jar new file mode 100644 index 00000000..48f36285 Binary files /dev/null and b/lib/de.ovgu.featureide.lib.fm-v3.9.1.jar differ diff --git a/lib/uvl-parser.jar b/lib/uvl-parser.jar new file mode 100644 index 00000000..06f5d818 Binary files /dev/null and b/lib/uvl-parser.jar differ diff --git a/src/main/java/edu/kit/provideq/toolbox/exception/ConversionException.java b/src/main/java/edu/kit/provideq/toolbox/exception/ConversionException.java new file mode 100644 index 00000000..e2830d2b --- /dev/null +++ b/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); + } +} diff --git a/src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/FeatureModelAnomalyController.java b/src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/FeatureModelAnomalyController.java new file mode 100644 index 00000000..d79ad031 --- /dev/null +++ b/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 { + + private final MetaSolver metaSolver; + + public FeatureModelAnomalyController(MetaSolver metaSolver) { + this.metaSolver = metaSolver; + } + + @Override + public ProblemType getProblemType() { + return ProblemType.FEATURE_MODEL_ANOMALY; + } + + @Override + public MetaSolver 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 getSolvers() { + return super.getSolvers(); + } +} diff --git a/src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/MetaSolverFeatureModelAnomaly.java b/src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/MetaSolverFeatureModelAnomaly.java new file mode 100644 index 00000000..b14ad69d --- /dev/null +++ b/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 { + + @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())); + } +} diff --git a/src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/SolveFeatureModelAnomalyRequest.java b/src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/SolveFeatureModelAnomalyRequest.java new file mode 100644 index 00000000..1a176e5f --- /dev/null +++ b/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 {} diff --git a/src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/solvers/FeatureModelAnomalySolver.java b/src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/solvers/FeatureModelAnomalySolver.java new file mode 100644 index 00000000..092fd609 --- /dev/null +++ b/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 problem) { + //TODO: assess problemData + return problem.type() == ProblemType.MAX_CUT; + } + + @Override + public float getSuitability(Problem problem) { + //TODO: implement algorithm for suitability calculation + return 1; + } + + @Override + public void solve(Problem problem, Solution 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(-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(-1); + satSolver.solve(new Problem<>(cnf, ProblemType.SAT), deadSolution); + + solution.setSolutionData(solutionBuilder.toString()); + } +} diff --git a/src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/solvers/FeatureModelSolver.java b/src/main/java/edu/kit/provideq/toolbox/featureModel/anomaly/solvers/FeatureModelSolver.java new file mode 100644 index 00000000..791bd9a5 --- /dev/null +++ b/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 { +} diff --git a/src/main/java/edu/kit/provideq/toolbox/featureModel/convert/UvlToDimacsCNF.java b/src/main/java/edu/kit/provideq/toolbox/featureModel/convert/UvlToDimacsCNF.java new file mode 100644 index 00000000..2e178ef2 --- /dev/null +++ b/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 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(); +// 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); + } +} diff --git a/src/main/java/edu/kit/provideq/toolbox/meta/ProblemType.java b/src/main/java/edu/kit/provideq/toolbox/meta/ProblemType.java index 5c501e1a..c885b855 100644 --- a/src/main/java/edu/kit/provideq/toolbox/meta/ProblemType.java +++ b/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. + * More information + */ + FEATURE_MODEL_ANOMALY, } diff --git a/src/main/java/edu/kit/provideq/toolbox/sat/convert/BoolExprToDimacsCNF.java b/src/main/java/edu/kit/provideq/toolbox/sat/convert/BoolExprToDimacsCNF.java index fba29492..ff27f331 100644 --- a/src/main/java/edu/kit/provideq/toolbox/sat/convert/BoolExprToDimacsCNF.java +++ b/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", "!") diff --git a/src/test/java/edu/kit/provideq/toolbox/featureModel/UvlToDimacsCNFTests.java b/src/test/java/edu/kit/provideq/toolbox/featureModel/UvlToDimacsCNFTests.java new file mode 100644 index 00000000..cc52404a --- /dev/null +++ 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 + """) + ); + } +}