Commit 17bf7348 authored by eder's avatar eder
Browse files

fixed extraction of annotation properties for DSML into SMT

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

Signed-off-by: default avatareder <eder@192.168.17.140>
parent e8537e6f
......@@ -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);
}
}
}
}
......
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