Commit bfc4760b authored by Alexander Diewald's avatar Alexander Diewald
Browse files

Merge branch '3641' into 'master'

3641

See merge request af3/af3!157
parents e96d52d6 cc44dfc8
Z3Backend.java 692e27caadbd9fa1fc2b83dfcef60dad752bdd3b GREEN
Z3Backend.java fbae87ebe57e64bcc657b79e64b17d58b49cdefd GREEN
......@@ -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;
......@@ -62,6 +67,7 @@ public class Z3Backend implements IDSEBackend {
throw new Exception("No exploration targets defined. Cannot perform DSE.");
}
List<SMTConstraint> basicCons = createBasicSignalConstraints(spec.getSearchSpace());
SolverRun solverRun;
if(solutionTypes.contains(Schedule.class) &&
solutionTypes.contains(TaskToExecutionUnitAllocationTable.class)) {
......@@ -71,7 +77,7 @@ 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()));
insertBasicConstraints(spec, basicCons);
if(isDebugVerboseEnabled()) {
System.out.println("DeploymentRun");
}
......@@ -84,9 +90,22 @@ public class Z3Backend implements IDSEBackend {
}
ExplorationSolution expSolution = solverRun.solve(spec, timeoutMS, monitor);
// remove basic constraints
spec.getTargets().removeAll(basicCons);
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;
......
......@@ -5,11 +5,11 @@ ConstraintDefinitionUtils.java f110a4a216905d2236324ae459d789d50114e25c GREEN
ConstraintToNonQuantifiedSMT.java de0e8a7000e26d745b62a27f8c2482e7a7737add GREEN
ConstraintToQuantifiedSMT.java c84e799c69195fe80a2e66a39d0192325b06c7fd GREEN
DSMLTransformationService.java b2e90e11e36346d01c79c18f16ffc62f66f35888 GREEN
DSMLtoSMTTransformator.java 7a03c75f6d7baba392fee2c0f900fb7726854d72 GREEN
DSMLtoSMTTransformator.java 8f4b1880e6a4ab9e8c69eb1c784d7320f6a6a500 RED
DeploScheduleRun.java d074d157250deba431d8f34d13d6464fd27f8acb GREEN
DeploymentRun.java 67d240b1f02f906748811acad9ced9dd71e7cb56 GREEN
IDSMLTransformationService.java f56241d2dff68a69cd1fe09c119d615f74088650 GREEN
SMTTransformationUtils.java d2aa072852daffcf3c439db7da5c639d807715a5 GREEN
ScheduleRun.java 1ced7f48c5067d32e029f577ace10cdbc597ed2d GREEN
SolverRun.java f73a675bcddf8a999dad1c33ec540b182ad1549e GREEN
SolverRun.java d00f743a184793fc5253069ff771044baeaeeb06 GREEN
TimingConstraintDefinition.java fba63bf61c53e7e6606a95515c20a7205f288f36 GREEN
......@@ -426,89 +426,86 @@ public class DSMLtoSMTTransformator {
private List<BoolExpr> extractProperties() throws UnsupportedDataTypeException, Z3Exception {
int duplicates = 0;
ArrayList<BoolExpr> results = new ArrayList<>();
List<Class<? extends IAnnotatedSpecification>> list = new ArrayList<>();
HashMap<Class<? extends IAnnotatedSpecification>, List<IModelElement>> map =
new HashMap<Class<? extends IAnnotatedSpecification>, List<IModelElement>>();
for(ExplorationTarget<?> expTarget : explorationSpec.getTargets()) {
if(expTarget instanceof SMTConstraint) {
SMTConstraint smtConstr = ((SMTConstraint)expTarget);
if(smtConstr.getContainedTargets().isEmpty()) {
extractAndAddProperties(list, smtConstr.getExpression());
extractAndAddProperties(map, smtConstr.getExpression());
} else {
for(ExplorationTarget<Boolean> target : smtConstr.getContainedTargets()) {
extractAndAddProperties(list, ((SMTConstraint)target).getExpression());
extractAndAddProperties(map, ((SMTConstraint)target).getExpression());
}
}
} else if(expTarget instanceof SMTObjective) {
SMTObjective smtObj = ((SMTObjective)expTarget);
if(!smtObj.getConstraints().isEmpty()) {
smtObj.getConstraints().stream()
.forEach(ot -> extractAndAddProperties(list, ot.getExpression()));
.forEach(ot -> extractAndAddProperties(map, ot.getExpression()));
}
extractAndAddProperties(list, smtObj.getExpression());
extractAndAddProperties(map, smtObj.getExpression());
}
}
for(Class<? extends IAnnotatedSpecification> specType : list) {
Map<Set<? extends IModelElement>, EnumSort> existingSorts =
transformationService.getExistingSorts();
for(Entry<Set<? extends IModelElement>, EnumSort> entry : existingSorts.entrySet()) {
final Set<?> setReference = entry.getKey();
for(IModelElement modelElement : setReference.getEntries()) {
IAnnotatedSpecification annotation = null;
IModelElement parameterProvider =
transformationService.getParameterProvider(modelElement, specType);
if(parameterProvider != null) {
annotation = getAnnotation(parameterProvider, specType);
}
Expr valueExpr = null;
if(annotation instanceof SafetyIntegrityLevel) {
Enumerator value = ((SafetyIntegrityLevel)annotation).getValue();
valueExpr = createInteger(context, value.getValue());
} else if(annotation instanceof HardwareCost) {
int value = ((HardwareCost)annotation).getCost();
valueExpr = createInteger(context, value);
} else if(annotation instanceof PowerConsumption) {
int value = ((PowerConsumption)annotation).getPower();
valueExpr = createInteger(context, value);
} else if(annotation instanceof TransmissionUnitBandwidth) {
double value = ((TransmissionUnitBandwidth)annotation).getBandwidth_MBitS();
valueExpr = createReal(context, Double.toString(value));
} else if(annotation instanceof FlashSize) {
long value = ((FlashSize)annotation).getBytes();
valueExpr = createInteger(context, value);
} else if(annotation instanceof RamSize) {
long value = ((RamSize)annotation).getBytes();
valueExpr = createInteger(context, value);
} else if(annotation instanceof FlashRequirement) {
long value = ((FlashRequirement)annotation).getBytes();
valueExpr = createInteger(context, value);
} else if(annotation instanceof RamRequirement) {
long value = ((RamRequirement)annotation).getBytes();
valueExpr = createInteger(context, value);
} else if(annotation instanceof FailureRate) {
double value = ((FailureRate)annotation).getFailureRate_FIT();
valueExpr = createReal(context, Double.toString(value));
}
for(Entry<Class<? extends IAnnotatedSpecification>, List<IModelElement>> mapEntry : map
.entrySet()) {
List<IModelElement> modelElements = mapEntry.getValue();
Class<? extends IAnnotatedSpecification> specType = mapEntry.getKey();
for(IModelElement model : modelElements) {
IAnnotatedSpecification annotation = null;
IModelElement parameterProvider =
transformationService.getParameterProvider(model, specType);
if(parameterProvider != null) {
annotation = getAnnotation(parameterProvider, specType);
}
Expr valueExpr = null;
if(annotation instanceof SafetyIntegrityLevel) {
Enumerator value = ((SafetyIntegrityLevel)annotation).getValue();
valueExpr = createInteger(context, value.getValue());
} else if(annotation instanceof HardwareCost) {
int value = ((HardwareCost)annotation).getCost();
valueExpr = createInteger(context, value);
} else if(annotation instanceof PowerConsumption) {
int value = ((PowerConsumption)annotation).getPower();
valueExpr = createInteger(context, value);
} else if(annotation instanceof TransmissionUnitBandwidth) {
double value = ((TransmissionUnitBandwidth)annotation).getBandwidth_MBitS();
valueExpr = createReal(context, Double.toString(value));
} else if(annotation instanceof FlashSize) {
long value = ((FlashSize)annotation).getBytes();
valueExpr = createInteger(context, value);
} else if(annotation instanceof RamSize) {
long value = ((RamSize)annotation).getBytes();
valueExpr = createInteger(context, value);
} else if(annotation instanceof FlashRequirement) {
long value = ((FlashRequirement)annotation).getBytes();
valueExpr = createInteger(context, value);
} else if(annotation instanceof RamRequirement) {
long value = ((RamRequirement)annotation).getBytes();
valueExpr = createInteger(context, value);
} else if(annotation instanceof FailureRate) {
double value = ((FailureRate)annotation).getFailureRate_FIT();
valueExpr = createReal(context, Double.toString(value));
}
if(valueExpr != null) {
ArithExpr z3Function =
transformationService.getZ3Function(specType, modelElement);
if(valueExpr != null) {
ArithExpr z3Function = transformationService.getZ3Function(specType, model);
final BoolExpr createEqual = createEqual(context, z3Function, valueExpr);
Collection<BoolExpr> filter2 =
filter(results, be -> be.toString().equals(createEqual.toString()));
final BoolExpr createEqual = createEqual(context, z3Function, valueExpr);
Collection<BoolExpr> filter2 =
filter(results, be -> be.toString().equals(createEqual.toString()));
Optional<BoolExpr> first = getFirst(filter2);
// if this assertion has already been added ignore it
if(!first.isPresent())
results.add(createEqual);
else {
duplicates++;
}
} else {
throw new UnsupportedDataTypeException(
specType.getSimpleName() + " is not yet implemented.");
Optional<BoolExpr> first = getFirst(filter2);
// if this assertion has already been added ignore it
if(!first.isPresent())
results.add(createEqual);
else {
duplicates++;
}
} else {
throw new UnsupportedDataTypeException(
specType.getSimpleName() + " is not yet implemented.");
}
}
}
......@@ -519,16 +516,28 @@ public class DSMLtoSMTTransformator {
}
/**
* Extracts the {@link IAnnotatedSpecification} out of all {@link ModelElementPropertyLiteral}
* sin the given {@link SMTConstraint} and adds it to the given list if it is not yet contained.
* Extracts all annotations and the respective model elements to which they apply, out of the
* given expression.
*/
private void extractAndAddProperties(List<Class<? extends IAnnotatedSpecification>> list,
private void extractAndAddProperties(
HashMap<Class<? extends IAnnotatedSpecification>, List<IModelElement>> map,
IExpression iExpression) {
final EList<ModelElementPropertyLiteral> childrenWithType =
getChildrenWithType(iExpression, ModelElementPropertyLiteral.class);
for(ModelElementPropertyLiteral mp : childrenWithType) {
if(!list.contains(mp.getSpecificationType())) {
list.add(mp.getSpecificationType());
List<IModelElement> modelElements;
Class<? extends IAnnotatedSpecification> spec = mp.getSpecificationType();
if(map.containsKey(spec)) {
modelElements = map.get(spec);
} else {
modelElements = new ArrayList<IModelElement>();
map.put(spec, modelElements);
}
for(IModelElement me : mp.getSetReference().getEntries()) {
if(!modelElements.contains(me)) {
modelElements.add(me);
}
}
}
}
......
......@@ -28,7 +28,6 @@ import static org.fortiss.af3.exploration.util.DesignSpaceExplorationModelElemen
import static org.fortiss.af3.exploration.util.DesignSpaceExplorationModelElementFactory.createSingleExplorationSolution;
import static org.fortiss.af3.exploration.util.ExplorationUtils.isDebugVerboseEnabled;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.pickInstanceOf;
import static org.fortiss.tooling.kernel.utils.KernelModelElementUtils.runAsCommand;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.info;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.warning;
......@@ -195,9 +194,7 @@ public abstract class SolverRun {
}
if(z3ModelSolutionAssocs != null && !z3ModelSolutionAssocs.isEmpty()) {
// Problem is solvable. At least one target must be present.
runAsCommand(explorationSpec.getTargets().get(0), () -> {
setSolutionModels(transformation);
});
setSolutionModels(transformation);
} else {
// Problem is not solvable.
parameters = new HashMap<>();
......
Markdown is supported
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