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

Exploration: Use SuperSets to pass model data to the backend.

* Modify (Super)Sets to use a generic that denotes the types of elements within a set. Thereby, it is ensured that only elements of this kind are contained/referenced in a specific set.
* Introduce a SuperSetMap that allows to associate the types of elements of supersets with superset instances.
* Use the SuperSetMap as the main entity to pass model elements from the DSE Project to backends.
* Add the ComponentToTaskAllocationTable to the DSESuperSet and the DSE model element: This is the new way to identify which Tasks belong to which Component.
refs 2939
parent 07754b8c
Z3Backend.java 127ff1bdc1a06231338512409df5230abcc91969 RED
Z3Backend.java 8638804600c4b193b7d0cca0f7016d15a8ffeb51 RED
......@@ -26,8 +26,8 @@ import org.eclipse.core.runtime.IProgressMonitor;
import org.fortiss.af3.deployment.model.Deployment;
import org.fortiss.af3.exploration.backend.DseSolutionVisualization;
import org.fortiss.af3.exploration.backend.IDseBackend;
import org.fortiss.af3.exploration.backend.IDseInputContainer;
import org.fortiss.af3.exploration.backend.RuleSetContainer;
import org.fortiss.af3.exploration.backend.SuperSetMap;
import org.fortiss.af3.exploration.model.ExplorationSolution;
import org.fortiss.af3.exploration.model.ExplorationSpecification;
import org.fortiss.af3.exploration.model.IExplorationFeature;
......@@ -71,17 +71,15 @@ public class Z3Backend implements IDseBackend {
// TODO: Currently, the DSE execute method is implemented using some Deployment synthesis
// specifics. These should be removed, as the method shall be generic.
public Optional<ExplorationSolution> executeDSE(RuleSetContainer spec,
Set<Class<? extends IModelElement>> solutionTypes, IDseInputContainer inputParameters,
Set<Class<? extends IModelElement>> solutionTypes, SuperSetMap superSetMap,
Collection<IExplorationFeature> explorationModules, IProgressMonitor monitor,
int timeoutMS) throws Exception {
if(spec.size() < 1) {
throw new Exception("No exploration targets defined. Cannot perform the DSE.");
}
DSESuperSets superSets = inputParameters.getInputModel(DSESuperSets.class);
DeploymentRun2 run = new DeploymentRun2();
DeploymentSMTResult isSolved = run.solveDeployment(spec, timeoutMS, monitor, superSets);
DeploymentSMTResult isSolved = run.solveDeployment(spec, timeoutMS, monitor, superSetMap);
// spec will not be empty (see entry condition).
ITopLevelElement context =
......
DSLtoSMT.java fa3ea9e12b97d1359e89d6c793018a247f5be1a6 RED
ScheduleRun.java dc655a85c0620eacbcd7bb1bd9ed296c12fdf1ce RED
SolverRun.java a82b92918eabf0d230ed8ec54eb1f020942cb849 RED
DSLtoSMT.java e12ce3bb3403de23b22070b2072e5e9979b2167e RED
ScheduleRun.java c07040dcdc506c2b9c82e4ed9ca559f9478b1f3b RED
SolverRun.java dc28d21b774cdf0b44a4b0ea760417605554c37d RED
......@@ -235,9 +235,8 @@ public class DSLtoSMT {
return createImplication(context, (BoolExpr)left, (BoolExpr)right);
}
} else if(expression instanceof IUnaryOperator<?>) {
Expr right =
toSMT(context, ((IUnaryOperator<IBooleanExpression>)expression).getRight(),
modelElements);
Expr right = toSMT(context, ((IUnaryOperator<IBooleanExpression>)expression).getRight(),
modelElements);
if(expression instanceof Not) {
return createNot(context, (BoolExpr)right);
}
......@@ -277,8 +276,8 @@ public class DSLtoSMT {
return z3Function;
}
}
throw new UnknownError("ModelElementPropertyLitral " + expression +
" cannot be resolved.");
throw new UnknownError(
"ModelElementPropertyLitral " + expression + " cannot be resolved.");
} else if(expression instanceof ArithmeticLiteral) {
// TODO(JE): value is 'casted' into integer. should be turned into a real expression
// in z3. Refs 2666
......@@ -296,9 +295,8 @@ public class DSLtoSMT {
String name = ((INamedCommentedElement)element).getName();
String simpleClassName = eClass.getSimpleName();
ArithExpr function =
(ArithExpr)createFunction(context, name + "_" + id + "_" + simpleClassName,
Z3Type.INT);
ArithExpr function = (ArithExpr)createFunction(context,
name + "_" + id + "_" + simpleClassName, Z3Type.INT);
return function;
}
......@@ -311,7 +309,9 @@ public class DSLtoSMT {
return (ArithExpr)createFunction(context, name + "_" + id, Z3Type.INT);
}
/** Creates a {@link BoolExpr} consisting of a comparison between two {@link ArithExpr}essions. */
/**
* Creates a {@link BoolExpr} consisting of a comparison between two {@link ArithExpr}essions.
*/
private static BoolExpr createComparisonExpression(Context context,
IComparisonExpression<?> booleanExpr, Expr left, Expr right) {
if(booleanExpr instanceof Greater) {
......@@ -342,12 +342,10 @@ public class DSLtoSMT {
Expr allocationSource = createFunction(context, source, Z3Type.INT);
allocationMapping.put(allocationSource, sourceModel);
// foo is used only to make the expression shorter
@SuppressWarnings("unused") boolean foo =
allocationSources.contains(sourceModel) ? false : allocationSources
.add(sourceModel);
foo =
allocationDestinations.contains(destinationModel) ? false : allocationDestinations
.add(destinationModel);
@SuppressWarnings("unused") boolean foo = allocationSources.contains(sourceModel) ? false
: allocationSources.add(sourceModel);
foo = allocationDestinations.contains(destinationModel) ? false
: allocationDestinations.add(destinationModel);
return createEqual(context, allocationSource, destination);
}
......@@ -363,9 +361,8 @@ public class DSLtoSMT {
// foo is used only to make the expression shorter
@SuppressWarnings("unused") boolean foo =
dislocationSources.contains(leftA) ? false : dislocationSources.add(leftA);
foo =
dislocationDestinations.contains(rightA) ? false : dislocationDestinations
.add(rightA);
foo = dislocationDestinations.contains(rightA) ? false
: dislocationDestinations.add(rightA);
BoolExpr equal = createEqual(context, dislocationSource, destination);
return createNot(context, equal);
}
......
......@@ -93,7 +93,8 @@ public class ScheduleRun extends SolverRun {
/**
* Solves the given {@link ExplorationSpecificationSubSet} and returns a {@link SystemSchedule}.
*/
public SystemSchedule solveSchedule(RuleSet subSet, int timeout, SystemSchedule systemSchedule) {
public SystemSchedule solveSchedule(RuleSet subSet, int timeout,
SystemSchedule systemSchedule) {
ArrayList<RuleSet> list = new ArrayList<>();
list.add(subSet);
return solveSchedule(list, timeout, systemSchedule);
......@@ -113,12 +114,10 @@ public class ScheduleRun extends SolverRun {
for(Entry<Expr, IModelElement> m : currentRun.startingTimeMapping.entrySet()) {
IntNum eval = (IntNum)model.eval(m.getKey(), true);
IModelElement modelElement = m.getValue();
EList<ResourceAllocation> childrenWithType =
EcoreUtils
.getChildrenWithType(systemSchedule, ResourceAllocation.class);
Optional<ResourceAllocation> findFirst =
childrenWithType.stream().filter(p -> p.equals(modelElement))
.findFirst();
EList<ResourceAllocation> childrenWithType = EcoreUtils
.getChildrenWithType(systemSchedule, ResourceAllocation.class);
Optional<ResourceAllocation> findFirst = childrenWithType.stream()
.filter(p -> p.equals(modelElement)).findFirst();
if(!findFirst.isPresent())
continue;
ResourceAllocation allocation = findFirst.get();
......@@ -159,9 +158,8 @@ public class ScheduleRun extends SolverRun {
int i = 0;
for(IBooleanExpression a : assertions) {
SMTConstraint ts =
Z3ModelElementFactory.createSMTConstraint(
"Implicit Schedule Constraint " + i++, a, true);
SMTConstraint ts = Z3ModelElementFactory
.createSMTConstraint("Implicit Schedule Constraint " + i++, a, true);
s.getExplorationTargets().add(ts);
}
assertions.stream().forEach(a -> System.out.println(a));
......@@ -169,19 +167,20 @@ public class ScheduleRun extends SolverRun {
}
/** Creates constraint for all start times to be greater or equal zero. */
private static List<? extends IBooleanExpression> createGreaterEqualZeroConstraints(
SystemSchedule schedule) {
private static List<? extends IBooleanExpression>
createGreaterEqualZeroConstraints(SystemSchedule schedule) {
List<IBooleanExpression> assertions = new ArrayList<>();
for(Schedule s : schedule.getScheduleList()) {
if(!(s instanceof ResourceSchedule)) {
System.err.println("Unkown schedule " + s +
"\nWill be ignored in schedule synthesis.");
System.err.println(
"Unkown schedule " + s + "\nWill be ignored in schedule synthesis.");
continue;
}
ResourceSchedule rs = (ResourceSchedule)s;
EList<ResourceAllocation> resourceAllocationList = rs.getResourceAllocationList();
Set set1 = createSet("AllResources_" + s.getName() + "_Set");
Set<IModelElement> set1 =
createSet("AllResources_" + s.getName() + "_Set", IModelElement.class);
set1.getEntries().addAll(resourceAllocationList);
ModelElementPropertyLiteral startSet1 =
......@@ -199,25 +198,28 @@ public class ScheduleRun extends SolverRun {
}
/** Creates the non overlapping constraint for the given schedule. */
public static List<IBooleanExpression> createNonOverlappingConstraints(SystemSchedule schedule) {
public static List<IBooleanExpression>
createNonOverlappingConstraints(SystemSchedule schedule) {
List<IBooleanExpression> assertions = new ArrayList<>();
for(Schedule s : schedule.getScheduleList()) {
if(!(s instanceof ResourceSchedule)) {
System.err.println("Unkown schedule " + s +
"\nWill be ignored in schedule synthesis.");
System.err.println(
"Unkown schedule " + s + "\nWill be ignored in schedule synthesis.");
continue;
}
ResourceSchedule rs = (ResourceSchedule)s;
// "Tasks" -> at the moment resource allocation is still referring to a component
EList<ResourceAllocation> tasks = rs.getResourceAllocationList();
Set set1 = createSet("aTasks_" + s.getName() + "_Set");
Set<IModelElement> set1 =
createSet("aTasks_" + s.getName() + "_Set", IModelElement.class);
set1.getEntries().addAll(tasks);
Set set2 = createSet("Tasks_" + s.getName() + "_Set2");
set2.getEntries().addAll(
tasks.stream().map(set -> EcoreUtils.copy(set)).collect(toList()));
Set<IModelElement> set2 =
createSet("Tasks_" + s.getName() + "_Set2", IModelElement.class);
set2.getEntries()
.addAll(tasks.stream().map(set -> EcoreUtils.copy(set)).collect(toList()));
ModelElementPropertyLiteral startSet1 =
createElementPropertyLiteral(set1, StartTimeDummy.class);
......@@ -268,7 +270,8 @@ public class ScheduleRun extends SolverRun {
// durations
for(Schedule a : schedule.getScheduleList()) {
for(ResourceAllocation rs : a.getResourceAllocationList()) {
Set oneElementSet = DSMLModelElementFactory.createSet(rs.getName() + "_set");
Set<IModelElement> oneElementSet = DSMLModelElementFactory
.createSet(rs.getName() + "_set", IModelElement.class);
oneElementSet.getEntries().add(rs);
ModelElementPropertyLiteral duration =
createElementPropertyLiteral(oneElementSet, DurationDummy.class);
......@@ -288,12 +291,10 @@ public class ScheduleRun extends SolverRun {
public static List<IBooleanExpression> createCausalityConstraints(SystemSchedule schedule) {
List<IBooleanExpression> assertions = new ArrayList<>();
// causality according to focus
List<Schedule> collect =
schedule.getScheduleList()
.stream()
.filter(s -> (s instanceof ResourceSchedule && ((ResourceSchedule)s)
.getResource() instanceof TransmissionUnit))
.collect(Collectors.toList());
List<Schedule> collect = schedule.getScheduleList().stream()
.filter(s -> (s instanceof ResourceSchedule &&
((ResourceSchedule)s).getResource() instanceof TransmissionUnit))
.collect(Collectors.toList());
for(Schedule s : collect) {
for(ResourceAllocation signal : s.getResourceAllocationList()) {
OutputPort modelElement =
......@@ -312,15 +313,18 @@ public class ScheduleRun extends SolverRun {
}
ForAll forAll1 = createForAll();
Set set1 = DSMLModelElementFactory.createSet("sourceTask");
Set<IModelElement> set1 = DSMLModelElementFactory.createSet("sourceTask",
IModelElement.class);
set1.getEntries().add(resourceAllocationSource);
forAll1.setSet(set1);
ForAll forAll2 = createForAll();
Set set2 = DSMLModelElementFactory.createSet("destinationTask");
Set<IModelElement> set2 = DSMLModelElementFactory
.createSet("destinationTask", IModelElement.class);
set2.getEntries().add(resourceAllocationTarget);
forAll2.setSet(set2);
ForAll forAll3 = createForAll();
Set set3 = DSMLModelElementFactory.createSet("mSignal");
Set<IModelElement> set3 =
DSMLModelElementFactory.createSet("mSignal", IModelElement.class);
set3.getEntries().add(signal);
forAll3.setSet(set3);
......
......@@ -206,9 +206,8 @@ public abstract class SolverRun {
for(IBinderExpression b : childrenWithType) {
List<IModelElement> collect;
final Stream<IModelElement> stream = b.getSet().getEntries().stream();
collect =
stream.filter(ent -> ent instanceof VirtualLink).collect(
Collectors.toList());
collect = stream.filter(ent -> ent instanceof VirtualLink)
.collect(Collectors.toList());
virtualLinks.addAll((Collection<? extends VirtualLink>)collect);
}
}
......@@ -230,8 +229,8 @@ public abstract class SolverRun {
LoggingUtils.info(AF3ExplorationSMTActivator.getDefault(),
"[Z3] solving problem with parameters " + solver.getParameterDescriptions());
Status check = solver.Check();
LoggingUtils.info(AF3ExplorationSMTActivator.getDefault(), "[Z3] " + check +
" Solved problem with parameters " + params);
LoggingUtils.info(AF3ExplorationSMTActivator.getDefault(),
"[Z3] " + check + " Solved problem with parameters " + params);
// optimize solver sometimes says unsat although it produces a result. because of this
// go on if the result list is not empty
if(check.equals(Status.UNSATISFIABLE) && models.isEmpty()) {
......@@ -257,35 +256,31 @@ public abstract class SolverRun {
*/
private List<BoolExpr> extractSignalAllocations(Context context,
HashMap<Expr, IModelElement> allocationMapping, List<VirtualLink> virtualLinks,
List<IModelElement> busesToMinimizeBw) throws UnsupportedDataTypeException, Z3Exception {
List<IModelElement> busesToMinimizeBw)
throws UnsupportedDataTypeException, Z3Exception {
List<BoolExpr> assertions = new ArrayList<>();
start = createFunction(context, "path_source", Z3Type.INT, Z3Type.INT);
destination = createFunction(context, "path_destination", Z3Type.INT, Z3Type.INT);
// function describing if a connection between two ecus is possible
ecuEcuPathMapping =
createFunction(context, "ecu_ecu_path_mapping", new Z3Type[] {Z3Type.INT,
Z3Type.INT}, Z3Type.BOOL);
ecuEcuPathMapping = createFunction(context, "ecu_ecu_path_mapping",
new Z3Type[] {Z3Type.INT, Z3Type.INT}, Z3Type.BOOL);
ecuEcuVirtualLinkMapping =
createFunction(context, "ecu_ecu_vl_mapping",
new Z3Type[] {Z3Type.INT, Z3Type.INT}, Z3Type.INT);
ecuEcuVirtualLinkMapping = createFunction(context, "ecu_ecu_vl_mapping",
new Z3Type[] {Z3Type.INT, Z3Type.INT}, Z3Type.INT);
pathCost = createFunction(context, "pathCost", Z3Type.INT, Z3Type.INT);
busPathMapping =
createFunction(context, "busPathMapping", new Z3Type[] {Z3Type.INT, Z3Type.INT},
Z3Type.BOOL);
busPathMapping = createFunction(context, "busPathMapping",
new Z3Type[] {Z3Type.INT, Z3Type.INT}, Z3Type.BOOL);
extractNotPossiblePaths(context, virtualLinks, assertions);
List<Entry<Expr, IModelElement>> channels =
allocationMapping.entrySet().stream().filter(e -> e.getValue() instanceof Channel)
.collect(toList());
List<Entry<Expr, IModelElement>> sourceComps =
allocationMapping.entrySet().stream()
.filter(e -> e.getValue() instanceof Component).collect(toList());
List<Entry<Expr, IModelElement>> channels = allocationMapping.entrySet().stream()
.filter(e -> e.getValue() instanceof Channel).collect(toList());
List<Entry<Expr, IModelElement>> sourceComps = allocationMapping.entrySet().stream()
.filter(e -> e.getValue() instanceof Component).collect(toList());
extractPathCosts(context, virtualLinks, assertions, channels);
......@@ -300,7 +295,8 @@ public abstract class SolverRun {
EObject target = targetPort.eContainer();
Expr sourceExpr = null, targetExpr = null;
while(!ComponentArchitectureUtils.isAtomicComponent((Component)targetPort.eContainer())) {
while(!ComponentArchitectureUtils
.isAtomicComponent((Component)targetPort.eContainer())) {
// follow the path to the next atomic component
Optional<Channel> findFirst = targetPort.getOutgoingChannels().stream().findFirst();
if(findFirst.isPresent()) {
......@@ -311,7 +307,8 @@ public abstract class SolverRun {
}
target = targetPort.eContainer();
while(!ComponentArchitectureUtils.isAtomicComponent((Component)sourcePort.eContainer())) {
while(!ComponentArchitectureUtils
.isAtomicComponent((Component)sourcePort.eContainer())) {
Optional<Channel> findFirst = sourcePort.getIncomingChannels().stream().findFirst();
if(findFirst.isPresent()) {
sourcePort = findFirst.get().getSource();
......@@ -376,12 +373,10 @@ public abstract class SolverRun {
ArithExpr busExpr2 = DSLtoSMT.getZ3Function(context, bus);
for(VirtualLink vl : virtualLinks) {
ArithExpr vlExpr = DSLtoSMT.getZ3Function(context, vl);
BoolExpr check =
Z3javaAPIWrapper.createEqual(context,
busPathMapping.apply(busExpr2, vlExpr), true);
Expr cost =
Z3javaAPIWrapper.createIfThenElse(context, check, pathCost.apply(vlExpr),
zero);
BoolExpr check = Z3javaAPIWrapper.createEqual(context,
busPathMapping.apply(busExpr2, vlExpr), true);
Expr cost = Z3javaAPIWrapper.createIfThenElse(context, check,
pathCost.apply(vlExpr), zero);
terms.add((ArithExpr)cost);
}
if(terms.isEmpty())
......@@ -413,9 +408,8 @@ public abstract class SolverRun {
for(Entry<Expr, IModelElement> c : channels) {
BoolExpr check = createEqual(context, c.getKey(), path);
Channel channel = (Channel)c.getValue();
TransmissionUnitBandwidth annot =
AnnotationUtils.getAnnotation(channel.getSource(),
TransmissionUnitBandwidth.class);
TransmissionUnitBandwidth annot = AnnotationUtils.getAnnotation(channel.getSource(),
TransmissionUnitBandwidth.class);
final int bandwidth_MBytesPerSecond = (int)annot.getBandwidth_MBytesPerSecond();
System.out.println(bandwidth_MBytesPerSecond);
IntNum bandwidth =
......@@ -557,33 +551,26 @@ public abstract class SolverRun {
if(target instanceof SMTConstraint) {
if(((SMTConstraint)target).getContainedTargets().isEmpty()) {
BoolExpr smt =
currentRun
.transfrom(context,
(IBooleanExpression)((SMTConstraint)target)
.getExpression());
BoolExpr smt = currentRun.transfrom(context,
(IBooleanExpression)((SMTConstraint)target).getExpression());
if(((SMTConstraint)target).isImplicit()) {
solver.add(smt);
} else {
BoolExpr b =
Z3javaAPIWrapper
.createBoolConst(context, "dummy" + smt.getId());
BoolExpr b = Z3javaAPIWrapper.createBoolConst(context,
"dummy" + smt.getId());
solver.assertAndTrack(smt, b);
constraintMapping.put(b, (SMTConstraint)target);
}
} else {
for(ExplorationTarget<Boolean> target2 : ((SMTConstraint)target)
.getContainedTargets()) {
BoolExpr smt =
currentRun.transfrom(context,
(IBooleanExpression)((SMTConstraint)target2)
.getExpression());
BoolExpr smt = currentRun.transfrom(context,
(IBooleanExpression)((SMTConstraint)target2).getExpression());
if(((SMTConstraint)target2).isImplicit()) {
solver.add(smt);
} else {
BoolExpr b =
Z3javaAPIWrapper.createBoolConst(context,
"dummy" + smt.getId());
BoolExpr b = Z3javaAPIWrapper.createBoolConst(context,
"dummy" + smt.getId());
solver.assertAndTrack(smt, b);
constraintMapping.put(b, (SMTConstraint)target2);
}
......@@ -607,10 +594,9 @@ public abstract class SolverRun {
EList<IBinderExpression> childrenWithType =
getChildrenWithType(tc.getExpression(), IBinderExpression.class);
for(IBinderExpression b : childrenWithType) {
List<IModelElement> collect =
b.getSet().getEntries().stream()
.filter(ent -> ent instanceof VirtualLink)
.collect(Collectors.toList());
List<IModelElement> collect = b.getSet().getEntries().stream()
.filter(ent -> ent instanceof VirtualLink)
.collect(Collectors.toList());
virtualLinks.addAll((Collection<? extends VirtualLink>)collect);
}
}
......@@ -618,13 +604,11 @@ public abstract class SolverRun {
}
}
final BoolExpr[] array =
extractSignalAllocations(context, allocationMapping, virtualLinks,
new ArrayList<>()).toArray(new BoolExpr[0]);
final BoolExpr[] array = extractSignalAllocations(context, allocationMapping, virtualLinks,
new ArrayList<>()).toArray(new BoolExpr[0]);
for(BoolExpr bex : array) {
BoolExpr b =
Z3javaAPIWrapper.createBoolConst(context, "signalDummy " + bex.toString() +
"|" + bex.getId());
BoolExpr b = Z3javaAPIWrapper.createBoolConst(context,
"signalDummy " + bex.toString() + "|" + bex.getId());
solver.assertAndTrack(bex, b);
}
......@@ -660,9 +644,8 @@ public abstract class SolverRun {
public static List<ExplorationObjective<?>> getOptimzations(List<RuleSet> subSets) {
List<ExplorationObjective<?>> results = new ArrayList<>();
for(RuleSet s : subSets) {
List<ExplorationTarget<?>> collect =
s.getExplorationTargets().stream()
.filter(c -> c instanceof ExplorationObjective<?>).collect(toList());
List<ExplorationTarget<?>> collect = s.getExplorationTargets().stream()
.filter(c -> c instanceof ExplorationObjective<?>).collect(toList());
results.addAll((Collection<? extends ExplorationObjective<?>>)collect);
}
return results;
......@@ -687,12 +670,11 @@ public abstract class SolverRun {
if(t instanceof SMTConstraint) {
SMTConstraint tc = ((SMTConstraint)t);
if(tc.getContainedTargets().isEmpty()) {
list.addAll(getChildrenWithType(tc.getExpression(),
ModelElementLiteral.class));
list.addAll(
getChildrenWithType(tc.getExpression(), ModelElementLiteral.class));
} else {
for(ExplorationTarget<Boolean> target : tc.getContainedTargets()) {
list.addAll(getChildrenWithType(
((SMTConstraint)target).getExpression(),
list.addAll(getChildrenWithType(((SMTConstraint)target).getExpression(),
ModelElementLiteral.class));
}
}
......@@ -729,8 +711,7 @@ public abstract class SolverRun {
ModelElementPropertyLiteral.class));
} else {
for(ExplorationTarget<Boolean> target : tc.getContainedTargets()) {
list.addAll(getChildrenWithType(
((SMTConstraint)target).getExpression(),
list.addAll(getChildrenWithType(((SMTConstraint)target).getExpression(),
ModelElementPropertyLiteral.class));
}
}
......@@ -742,7 +723,7 @@ public abstract class SolverRun {
}
for(ModelElementPropertyLiteral m : list) {
for(IModelElement model : m.getSetReference().getEntries()) {
for(IModelElement model : new ArrayList<>(m.getSetReference().getEntries())) {
Class<? extends IAnnotatedSpecification> specificationType =
m.getSpecificationType();
// ignire dummy schedule elements
......@@ -783,9 +764,8 @@ public abstract class SolverRun {
// valueExpr = Z3javaAPIWrapper.createInteger(context, value);
}
} else if(annotation instanceof TransmissionUnitBandwidth) {
int value =
(int)((TransmissionUnitBandwidth)annotation)
.getBandwidth_MBytesPerSecond();
int value = (int)((TransmissionUnitBandwidth)annotation)
.getBandwidth_MBytesPerSecond();
valueExpr = Z3javaAPIWrapper.createInteger(context, value);
} else if(annotation instanceof Flash) {
int value = ((Flash)annotation).getMemory();
......@@ -798,8 +778,8 @@ public abstract class SolverRun {
if(valueExpr != null) {
results.add(createEqual(context, z3Function, valueExpr));
} else {
throw new UnsupportedDataTypeException(annotation.getClass()
.getSimpleName() + " is not yet implemented.");
throw new UnsupportedDataTypeException(
annotation.getClass().getSimpleName() + " is not yet implemented.");
}
}
}
......
BasicDeploymentConstraint.java ec1b6690abd47c5a6ee9c2e1c9e62828e2f15ff5 RED
ConstraintToNONQuantifiedSMT.java c25cd81671ebea484377cd58e094a5d8e4b0e812 RED
ConstraintToQuantifiedSMT.java 181a0190b1586982af5ce8a02a927f6512ee3b30 RED
DeploymentRun2.java 6687b5a978f3de55c64cc10d8873c77ff242d6f4 RED
ITransformationService.java f2fbdb2b1abd59b5fbc38fc1e8543ab6a5752f2a RED
LanguageTransformation.java 48f751551ef0c018bf56398853a3ffec68a77cb8 RED
SMTTransformationUtils.java 66657c85272ce6170c4b63d816680dbb07a45a1b RED
BasicDeploymentConstraint.java 20b61cba24661109cbffb2548042f54ae4c3d7e0 RED
ConstraintToNONQuantifiedSMT.java 99f852223c25442c395ff888cabbcc3b18694a5a RED
ConstraintToQuantifiedSMT.java 9cbb27b1ac997015a642a652351c96ec726a35d5 RED
DeploymentRun2.java 4eaef8648a4815b61cb89187cddb3181210f8da8 RED
ITransformationService.java fcddb7beb90eb693983babba30728d4600c15fc6 RED
LanguageTransformation.java 533f2d36fc76fbff13e7ee72da1eb47ea6d1c1a6 RED
SMTTransformationUtils.java c7a344d8141974b01dbcd6f9b89f8c4a4af668db RED
SolverRun2.java a00cf83a55691f64e3afd45b122b33103b884718 RED
TransformationService.java 0c6a1241b2860118fef1198ae04e82bee58a1587 RED