Evaluation bundle for comparison of different approaches

bundles/dev.arcovia.mitigation.ilp/src/dev/arcovia/mitigation/ilp/Constraint.java

@@ -54,7 +54,7 @@ public boolean isMatched(DFDVertex vertex) {
 			}
 		};
 		this.mitigations = determineMitigations();
-
+		setPreconditionLabels();
 	}
 
 	public Constraint(List<MitigationStrategy> mitigations) {
@@ -72,18 +72,7 @@ public List<MitigationStrategy> getMitigations() {
 	}
 
 	public boolean isPrecondition(CompositeLabel label) {
-		if (dslConstraint == null) {
-			return preconditionLabel.contains(label);
-		}
-		var translation = new CNFTranslation(dslConstraint);
-		var literals = translation.constructCNF().get(0).literals();
-
-		for (var literal : literals) {
-			if (!literal.positive() && literal.compositeLabel().equals(label)) {
-				return true;
-			}
-		}
-		return false;
+	    return preconditionLabel.contains(label);
 	}
 
 	public void addPrecondition(CompositeLabel label) {
@@ -112,6 +101,12 @@ public void findAlternativeMitigations() {
 	public Set<Node> determineViolations(DFDFlowGraphCollection flowGraph) {
 		return evaluationFunction.evaluate(flowGraph);
 	}
+
+	private void setPreconditionLabels(){
+        for (var lit : new CNFTranslation(dslConstraint).constructCNF().get(0).literals()) {
+            if (!lit.positive()) preconditionLabel.add(lit.compositeLabel());
+        }
+    }
 
 	private Set<Node> getDSLViolations(DFDFlowGraphCollection flowGraph) {
 		Set<Node> violatingNodes = new HashSet<>();

bundles/dev.arcovia.mitigation.ilp/src/dev/arcovia/mitigation/ilp/ILPSolver.java

@@ -137,27 +137,37 @@ public List<Mitigation> solve(List<List<Mitigation>> mitigations, Set<Mitigation
 
 		MPSolver.ResultStatus status = solver.solve();
 
-		if (status == MPSolver.ResultStatus.OPTIMAL || status == MPSolver.ResultStatus.FEASIBLE) {
-			List<Mitigation> chosen = new ArrayList<>();
-			for (MPVariable variable : solver.variables()) {
-				if (variable.solutionValue() > 0.5) {
-					// skip auxiliary variables introduced by required semantic
-					if (variable.name().startsWith("required_") || variable.name().startsWith("y_")) {
-						continue;
-					}
-
-					Optional<Mitigation> mitigation = allMitigations.stream()
-							.filter(m -> variable.name().equals(m.toString())).findFirst();
-					if (mitigation.isPresent()) {
-						chosen.add(mitigation.get());
-					}
-				}
-			}
-			return chosen;
-		} else {
-			System.out.println("No feasible solution: " + status);
-			return null;
+		try {
+		    if (status == MPSolver.ResultStatus.OPTIMAL || status == MPSolver.ResultStatus.FEASIBLE) {
+	            List<Mitigation> chosen = new ArrayList<>();
+	            for (MPVariable variable : solver.variables()) {
+	                if (variable.solutionValue() > 0.5) {
+	                    // skip auxiliary variables introduced by required semantic
+	                    if (variable.name().startsWith("required_") || variable.name().startsWith("y_")) {
+	                        continue;
+	                    }
+
+	                    Optional<Mitigation> mitigation = allMitigations.stream()
+	                            .filter(m -> variable.name().equals(m.toString())).findFirst();
+	                    if (mitigation.isPresent()) {
+	                        chosen.add(mitigation.get());
+	                    }
+	                }
+	            }
+	            return chosen;
+	        } else {
+	            System.out.println("No feasible solution: " + status);
+	            return null;
+	        }
 		}
+		finally {
+            // Explicitly free the native SCIP instance now rather than waiting for GC.
+            // Without this, the finalizer of a previous MPSolver may run during a later
+            // test's solve() call and corrupt SCIP's global state, causing sync_status_
+            // to reset to MUST_RELOAD even when Solve() returned OPTIMAL.
+            solver.delete();
+        }
+
 	}
 
 	/***

bundles/dev.arcovia.mitigation.ilp/src/dev/arcovia/mitigation/ilp/Node.java

@@ -66,7 +66,7 @@ public List<AbstractVertex<?>> getPrevious() {
 		return previous;
 	}
 
-	public List<Mitigation> getPossibleMitigations() {
+	public List<Mitigation> getPossibleMitigations(boolean restrictedToAdding) {
 		List<Mitigation> mitigations = new ArrayList<>();
 		for (var constraint : violatingConstraints) {
 			for (var mitigation : constraint.getMitigations()) {
@@ -79,41 +79,56 @@ public List<Mitigation> getPossibleMitigations() {
 					mitigations.addAll(getDataMitigations(mitigation, ActionType.Adding));
 				}
 				case DeleteNodeLabel -> {
-					mitigation.checkIfAllowed(vertex);
-					mitigations.add(new Mitigation(new ActionTerm(this.name, mitigation.label, ActionType.Removing),
-							mitigation.cost, getAllRequiredMitigations(mitigation)));
+					if (!restrictedToAdding) {
+						mitigation.checkIfAllowed(vertex);
+						mitigations.add(new Mitigation(new ActionTerm(this.name, mitigation.label, ActionType.Removing),
+								mitigation.cost, getAllRequiredMitigations(mitigation)));
+					}
 				}
 				case DeleteDataLabel -> {
-					mitigations.addAll(getDataMitigations(mitigation, ActionType.Removing));
+					if (!restrictedToAdding) {
+						mitigations.addAll(getDataMitigations(mitigation, ActionType.Removing));
+					}
 				}
 				case AddNode -> {
-					if (this.outgoingFlow == null) {
-						mitigations.add(new Mitigation(new ActionTerm(this.name, mitigation.label, ActionType.AddSink),
-								mitigation.cost, getAllRequiredMitigations(mitigation)));
-					} else {
-						mitigations.add(new Mitigation(
-								new ActionTerm(this.outgoingFlow.getId(), mitigation.label, ActionType.AddNode),
-								mitigation.cost, getAllRequiredMitigations(mitigation)));
-						mitigations.addAll(getNodeAdditionMitigations(mitigation));
+					if (!restrictedToAdding) {
+						if (this.outgoingFlow == null) {
+							mitigations
+									.add(new Mitigation(new ActionTerm(this.name, mitigation.label, ActionType.AddSink),
+											mitigation.cost, getAllRequiredMitigations(mitigation)));
+						} else {
+							mitigations.add(new Mitigation(
+									new ActionTerm(this.outgoingFlow.getId(), mitigation.label, ActionType.AddNode),
+									mitigation.cost, getAllRequiredMitigations(mitigation)));
+							mitigations.addAll(getNodeAdditionMitigations(mitigation));
+						}
+
 					}
 
 				}
 				case AddSink -> {
-					mitigations.add(new Mitigation(new ActionTerm(this.name, mitigation.label, ActionType.AddSink),
-							mitigation.cost, getAllRequiredMitigations(mitigation)));
-					mitigations.addAll(getSinkAdditionMitigations(mitigation));
+					if (!restrictedToAdding) {
+						mitigations.add(new Mitigation(new ActionTerm(this.name, mitigation.label, ActionType.AddSink),
+								mitigation.cost, getAllRequiredMitigations(mitigation)));
+						mitigations.addAll(getSinkAdditionMitigations(mitigation));
+					}
 				}
 				case DeleteNode -> {
-					mitigations.add(new Mitigation(new ActionTerm(this.name, mitigation.label, ActionType.RemoveNode),
-							mitigation.cost, getAllRequiredMitigations(mitigation)));
-				}
-				case DeleteFlow -> {
-					for (var incomingFlow : this.vertex.getPinFlowMap().values()) {
+					if (!restrictedToAdding) {
 						mitigations
-								.add(new Mitigation(new ActionTerm(incomingFlow.getId(), null, ActionType.RemoveFlow),
+								.add(new Mitigation(new ActionTerm(this.name, mitigation.label, ActionType.RemoveNode),
 										mitigation.cost, getAllRequiredMitigations(mitigation)));
 					}
 				}
+				case DeleteFlow -> {
+					if (!restrictedToAdding) {
+						for (var incomingFlow : this.vertex.getPinFlowMap().values()) {
+							mitigations.add(
+									new Mitigation(new ActionTerm(incomingFlow.getId(), null, ActionType.RemoveFlow),
+											mitigation.cost, getAllRequiredMitigations(mitigation)));
+						}
+					}
+				}
 
 				default -> throw new IllegalArgumentException("Unexpected value: " + mitigation.type);
 
@@ -194,8 +209,7 @@ private List<List<Mitigation>> getAllRequiredMitigations(MitigationStrategy miti
 				ActionType type;
 				if (mitgation.type.toString().startsWith("Delete")) {
 					type = ActionType.Removing;
-				}
-				else if (mitgation.type == MitigationType.AddNode) {
+				} else if (mitgation.type == MitigationType.AddNode) {
 					type = ActionType.AddNode;
 				} else if (mitgation.type == MitigationType.AddSink) {
 					type = ActionType.AddSink;

bundles/dev.arcovia.mitigation.ilp/src/dev/arcovia/mitigation/ilp/OptimizationManager.java

@@ -28,10 +28,11 @@
 
 import dev.arcovia.mitigation.sat.CompositeLabel;
 import dev.arcovia.mitigation.sat.LabelCategory;
+import dev.arcovia.mitigation.sat.MitigationApproach;
 import dev.arcovia.mitigation.sat.NodeLabel;
 import dev.arcovia.mitigation.sat.timeMeasurement;
 
-public class OptimizationManager {
+public class OptimizationManager implements MitigationApproach{
 	private final DataFlowDiagramAndDictionary dfd;
 
 	Map<String, String> outPinToAssignmentMap = new HashMap<>();
@@ -50,6 +51,8 @@ public class OptimizationManager {
 	private List<ActionTerm> actions;
 
 	private List<Mitigation> result;
+
+	private boolean isRestritedToLabelAddition = false;
 
 	public OptimizationManager(String dfdLocation, List<AnalysisConstraint> constraints) {
 		this.dfd = new Web2DFDConverter().convert(new WebEditorConverterModel(dfdLocation));
@@ -91,14 +94,19 @@ public DataFlowDiagramAndDictionary repair() throws Exception {
 		analyseDFD();
 
 		for (var node : violatingNodes) {
-			addMitigations(node.getPossibleMitigations());
+			addMitigations(node.getPossibleMitigations(isRestritedToLabelAddition));
 		}
 
 		for (var mitigation : allMitigations) {
 			if (mitigation.mitigation().type().toString().startsWith("Remove")) {
 				contradictions.addAll(determineContradictions(mitigation));
 			}
 		}
+
+		//if no violation found return dfd
+        if (mitigations.isEmpty()) {
+            return dfd;
+        }
 
 		var solver = new ILPSolver();
 		result = solver.solve(mitigations, allMitigations, contradictions);
@@ -121,14 +129,21 @@ public DataFlowDiagramAndDictionary repair(timeMeasurement timer) throws Excepti
 		timer.analysis();
 
 		for (var node : violatingNodes) {
-			addMitigations(node.getPossibleMitigations());
+			addMitigations(node.getPossibleMitigations(isRestritedToLabelAddition));
 		}
 
 		for (var mitigation : allMitigations) {
 			if (mitigation.mitigation().type().toString().startsWith("Remove")) {
 				contradictions.addAll(determineContradictions(mitigation));
 			}
 		}
+
+		//if no violation found return dfd
+        if (mitigations.isEmpty()) {
+        	timer.solving();
+        	timer.stop();
+            return dfd;
+        }
 
 		var solver = new ILPSolver();
 		result = solver.solve(mitigations, allMitigations, contradictions);
@@ -143,7 +158,12 @@ public DataFlowDiagramAndDictionary repair(timeMeasurement timer) throws Excepti
 
 		return dfd;
 	}
-
+
+	@Override
+	public void restrictToLabelAddition() {
+		isRestritedToLabelAddition = true;
+	}
+
 	public int getCost() {
 		int cost = 0;
 		for (var mitigation : result) {
@@ -448,12 +468,9 @@ private void addNodes(DataFlowDiagramAndDictionary dfd, List<ActionTerm> actions
 				var flow = dataFlowDiagram.getFlows().stream().filter(f -> f.getId().equals(action.domain()))
 						.findFirst().orElseThrow();
 
-				var node = flow.getSourceNode();
-
 				var name = action.compositeLabels().get(0).label().value();
 
-				var behaviorOld = node.getBehavior();
-
+
 				var dfdFactory = dataflowdiagramFactory.eINSTANCE;
 
 				var vertex = dfdFactory.createProcess();
@@ -481,8 +498,6 @@ private void addNodes(DataFlowDiagramAndDictionary dfd, List<ActionTerm> actions
 
 				behaviorNew.getInPin().add(inPin);
 
-				Set<Label> allLabels = new HashSet<>();
-
 				var sink = flow.getDestinationNode();
 				var inPinOld = flow.getDestinationPin();
 
@@ -758,7 +773,6 @@ private void removeNodes(DataFlowDiagramAndDictionary dfd, List<ActionTerm> acti
 	}
 
 	private void removeFlows(DataFlowDiagramAndDictionary dfd, List<ActionTerm> actions) {
-		var dd = dfd.dataDictionary();
 		var dataFlowDiagram = dfd.dataFlowDiagram();
 		for (var action : actions) {
 			if (action.type().equals(ActionType.RemoveFlow)) {

bundles/dev.arcovia.mitigation.sat/src/dev/arcovia/mitigation/sat/Mechanic.java

@@ -37,7 +37,7 @@
  * constraints and repairing violations found within the DFD. It provides the ability to assess whether a DFD and its
  * constraints are consistent and suggests corrections to resolve violations.
  */
-public class Mechanic {
+public class Mechanic implements MitigationApproach{
     Map<String, String> outPinToAss = new HashMap<>();
 
     private final DataFlowDiagramAndDictionary dfd;
@@ -181,6 +181,12 @@ public DataFlowDiagramAndDictionary repair() throws ContradictionException, Time
         }
 
         var solutions = new Sat().solve(nodes, flows, constraints, dfdName, deactivateSubsumption, allLabels);
+
+        if(solutions.isEmpty()) {
+        	logger.error("No solution found!");
+        	return dfd;
+        }
+
         List<Term> flatendNodes = getFlatNodes(nodes);
 
         List<Term> chosenSolution = getChosenSolution(solutions, flatendNodes);
@@ -715,4 +721,9 @@ private org.dataflowanalysis.dfd.datadictionary.Label getOrCreateLabel(DataDicti
         }
         return label;
     }
+
+	@Override
+	public void restrictToLabelAddition() {
+		// already restricted due to design		
+	}
 }

bundles/dev.arcovia.mitigation.sat/src/dev/arcovia/mitigation/sat/MitigationApproach.java

@@ -0,0 +1,9 @@
+package dev.arcovia.mitigation.sat;
+
+import org.dataflowanalysis.converter.dfd2web.DataFlowDiagramAndDictionary;
+
+
+public interface MitigationApproach {
+	DataFlowDiagramAndDictionary repair() throws Exception;
+    void restrictToLabelAddition();
+}

bundles/dev.arcovia.mitigation.sat/src/dev/arcovia/mitigation/sat/Sat.java

@@ -44,7 +44,8 @@ public class Sat {
     private boolean deactivateSubsumption;
     private Set<Label> allLabels = null;
 
-    private static final boolean SCALINGTEST = false;
+    private static final boolean SCALING_TEST = false;
+    private static final int TERMINATION_THRESHOLD = Integer.MAX_VALUE;
 
     /**
      * Solves a constraint satisfaction problem based on the given nodes, flows, and constraints. The method builds the
@@ -129,8 +130,8 @@ private List<List<Term>> solveClauses() throws TimeoutException, ContradictionEx
             if (!negated.isEmpty() && !deactivateSubsumption)
                 addClause(negated);
 
-            if (solutions.size() > 10000) {
-                if (deactivateSubsumption || SCALINGTEST)
+            if (solutions.size() > TERMINATION_THRESHOLD) {
+                if (deactivateSubsumption || SCALING_TEST)
                     return solutions;
 
                 throw new TimeoutException("Solving needed to be terminated after finding 10.000 solutions");