Commit 31d9e076 authored by Johannes Eder's avatar Johannes Eder
Browse files

RED, TODOs/FIXMEs to be discussed

refs 3201
parent 69514d33
BasicDeploymentConstraint.java 1be5c6e9373e5e320891e3c945f329146ca1f621 YELLOW
ConstraintToNONQuantifiedSMT.java 99f852223c25442c395ff888cabbcc3b18694a5a RED
ConstraintToQuantifiedSMT.java 9cbb27b1ac997015a642a652351c96ec726a35d5 RED
DeploymentRun2.java 6e23c25d311b8f7decbc683943d0f38fb63f2bb6 RED
DeploymentRun2.java decc21b8d3b6d44b27d594b61dce8f98d4f946dd RED
ITransformationService.java fcddb7beb90eb693983babba30728d4600c15fc6 RED
LanguageTransformation.java dec787bc76da370eb066356b9192bddd86aeb290 RED
SMTTransformationUtils.java e0002fedbebe5fc5386d63b114ccb4e29afba26b YELLOW
......
......@@ -33,17 +33,18 @@ import org.fortiss.af3.exploration.model.ExplorationSpecification;
import org.fortiss.af3.exploration.model.SuperSetMap;
import org.fortiss.af3.exploration.model.solutions.ExplorationSolution;
import org.fortiss.af3.exploration.model.solutions.SingleExplorationSolution;
import org.fortiss.af3.exploration.projectmodel.RuleSet;
import org.fortiss.af3.exploration.smt.AF3ExplorationSMTActivator;
import org.fortiss.af3.platform.model.allocation.ComponentToExecutionUnitAllocationEntry;
import org.fortiss.af3.platform.model.allocation.ComponentToExecutionUnitAllocationTable;
import org.fortiss.af3.task.model.allocation.ComponentToTaskAllocationEntry;
import org.fortiss.tooling.kernel.utils.LoggingUtils;
import com.microsoft.z3.Context;
import com.microsoft.z3.Model;
import com.microsoft.z3.Z3Exception;
/**
* Class for generating deployment via SMT solver. Uses {@link RuleSet}s as
* Class for generating deployment via SMT solver. Uses an {@link ExplorationSpecification} as
* input.
*
* @author eder
......@@ -52,11 +53,18 @@ public class DeploymentRun2 extends SolverRun2 {
/** List of the latest deployment results. */
protected Collection<ComponentToExecutionUnitAllocationTable> result;
// TODO(AD): @param should be used to describe the parameters (here: timeout). Also, it would
// increase the readability if a one sentence description of RuleSets could be give.
/**
* Solves the given {@link RuleSet}s and returns a list of allocations
* (deployment). Timeout in ms.
* Solves the given {@link ExplorationSpecification} and returns a list
* {@link ExplorationSolution}. Timeout in ms.
*
* @param explorationSpec
* {@link ExplorationSpecification} describing the dse deployment problem.
* @param timeout
* The timeout for the solver in ms.
* @param monitor
* A {@link IProgressMonitor} if the progress should be visible in the gui. Can also
* be null.
* @return {@link ExplorationSolution} including the deployment(s) if existing
*/
public ExplorationSolution solveDeployment(ExplorationSpecification explorationSpec,
int timeout, IProgressMonitor monitor) {
......@@ -86,8 +94,7 @@ public class DeploymentRun2 extends SolverRun2 {
// however, not clean since we expect two return types: the list of model elements + the
// solver state. We can discuss, whether the transformation should be shifted inside the
// below method such that we obtain a single return value via the exploration solution.
solveOptimized(context, numberOfRuns, timeout, transformation, explorationSpec,
monitor);
solveOptimized(context, numberOfRuns, timeout, transformation, explorationSpec, monitor);
if(z3ModelSolutionAssocs != null && !z3ModelSolutionAssocs.isEmpty()) {
// Problem is solvable.
// UNKNOWN produces result but may not be optimal and not be valid
......@@ -100,16 +107,11 @@ public class DeploymentRun2 extends SolverRun2 {
ps.put("timeout", timeout + "");
ps.put("unsat_core", "true");
context = new Context(ps);
solveNonOptimized(context, timeout,
new LanguageTransformation(explorationSpec, context, superSets, ctAllocs),
expSolution);
solveNonOptimized(context, timeout, new LanguageTransformation(explorationSpec,
context, superSets, ctAllocs), expSolution);
}
} catch(Z3Exception e) {
// TODO(AD): Use LoggingUtils from the kernel/base.
e.printStackTrace();
} catch(UnsupportedDataTypeException e) {
// TODO(AD): Use LoggingUtils from the kernel/base.
e.printStackTrace();
} catch(Z3Exception | UnsupportedDataTypeException e) {
LoggingUtils.error(AF3ExplorationSMTActivator.getDefault(), e.getMessage());
}
return expSolution;
}
......
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