Commit 31c5dcfe authored by eder's avatar eder
Browse files

# WARNING: head commit changed in the meantime

fixed bug by inserting basic constraints at beginning of exploration
spec

Issue-Ref: 3626
Issue-Url: https://af3-developer.fortiss.org/issues/3626



Signed-off-by: default avatareder <eder@10.0.5.223>
parent ea6ccbb6
Z3Backend.java 692e27caadbd9fa1fc2b83dfcef60dad752bdd3b GREEN
Z3Backend.java 5eddc51c874d6d89074702b4f217f0763b398db6 YELLOW
......@@ -18,17 +18,22 @@ package org.fortiss.af3.exploration.smt.backend;
import static org.fortiss.af3.exploration.smt.modeltransformation.BasicDeploymentConstraint.createBasicSignalConstraints;
import static org.fortiss.af3.exploration.util.ExplorationUtils.isDebugVerboseEnabled;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashSet;
import java.util.List;
import java.util.Optional;
import java.util.Set;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.emf.common.util.EList;
import org.fortiss.af3.exploration.model.ExplorationSpecification;
import org.fortiss.af3.exploration.model.ExplorationTarget;
import org.fortiss.af3.exploration.model.IExplorationFeature;
import org.fortiss.af3.exploration.model.solutions.ExplorationSolution;
import org.fortiss.af3.exploration.service.DSESolutionVisualization;
import org.fortiss.af3.exploration.service.IDSEBackend;
import org.fortiss.af3.exploration.smt.model.SMTConstraint;
import org.fortiss.af3.exploration.smt.modeltransformation.DeploScheduleRun;
import org.fortiss.af3.exploration.smt.modeltransformation.DeploymentRun;
import org.fortiss.af3.exploration.smt.modeltransformation.ScheduleRun;
......@@ -71,7 +76,8 @@ public class Z3Backend implements IDSEBackend {
solverRun = new DeploScheduleRun();
} else if(solutionTypes.contains(TaskToExecutionUnitAllocationTable.class)) {
// Add SMT-specific constraints to define the basic deployment problem.
spec.getTargets().addAll(createBasicSignalConstraints(spec.getSearchSpace()));
List<SMTConstraint> basicCons = createBasicSignalConstraints(spec.getSearchSpace());
insertBasicConstraints(spec, basicCons);
if(isDebugVerboseEnabled()) {
System.out.println("DeploymentRun");
}
......@@ -87,6 +93,17 @@ public class Z3Backend implements IDSEBackend {
return Optional.of(expSolution);
}
/** Inserts the given constraints at the beginning of the {@link ExplorationSpecification}. */
private void insertBasicConstraints(ExplorationSpecification spec,
List<SMTConstraint> basicCons) {
EList<ExplorationTarget<?>> targets = spec.getTargets();
List<ExplorationTarget<?>> temp = new ArrayList<>();
temp.addAll(targets);
spec.getTargets().clear();
spec.getTargets().addAll(basicCons);
spec.getTargets().addAll(temp);
}
/** Returns the cached solution representation (metrics/visualization + solution models). */
public DSESolutionVisualization getSolutionVisualization() {
return solutionVisualization;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment