Commit aa76f374 authored by Simon Barner's avatar Simon Barner

Merge branch 'master' of https://git.fortiss.org/af3/af3.git into 3935

parents 8f90bd63 640686cb
model.ecore 05b413982198507b12ffa9243342741a501af3fe GREEN
model.ecore 3159422b58b66acc4c36ccc8e318a2b9b1773da5 GREEN
......@@ -36,16 +36,6 @@
</eAnnotations>
</eStructuralFeatures>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="StartTimeDummy" eSuperTypes="platform:/resource/org.fortiss.tooling.base/model/base.ecore#//element/IAnnotatedSpecification platform:/resource/org.fortiss.tooling.base/model/base.ecore#//element/IHiddenSpecification">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
<details key="documentation" value="Dummy anntotation to describe the start time of a model element."/>
</eAnnotations>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="DurationDummy" eSuperTypes="platform:/resource/org.fortiss.tooling.base/model/base.ecore#//element/IAnnotatedSpecification platform:/resource/org.fortiss.tooling.base/model/base.ecore#//element/IHiddenSpecification">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
<details key="documentation" value="Dummy anntotation to describe the duration of a model element."/>
</eAnnotations>
</eClassifiers>
<eSubpackages name="dseml" nsURI="http://www.fortiss.org/af3/exploration/smt/dseml"
nsPrefix="org-fortiss-af3-exploration-smt-dseml">
<eClassifiers xsi:type="ecore:EClass" name="FrequencyAssigned" eSuperTypes="platform:/resource/org.fortiss.af3.exploration/model/dseml.ecore#//function/IFunction platform:/resource/org.fortiss.af3.exploration/model/dseml.ecore#//arithmetic/ArithmeticLiteral">
......
......@@ -16,8 +16,6 @@
<genClasses ecoreClass="model.ecore#//CustomDimension">
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute model.ecore#//CustomDimension/dimension"/>
</genClasses>
<genClasses ecoreClass="model.ecore#//StartTimeDummy"/>
<genClasses ecoreClass="model.ecore#//DurationDummy"/>
<nestedGenPackages prefix="Dseml" basePackage="org.fortiss.af3.exploration.smt.model"
disposableProviderFactory="true" ecorePackage="model.ecore#//dseml">
<genClasses ecoreClass="model.ecore#//dseml/FrequencyAssigned">
......
BasicDeploScheduleConstraint.java 89ed2c85c098ae98a58086f587a440dc3c437d0c GREEN
BasicDeploScheduleConstraint.java 95c1a55dd30de0b62ab7da3aa7055ed446f8e01b GREEN
BasicDeploymentConstraint.java f66c59adfa5a1619db1f1178c95fe7a4b7930d6e GREEN
BasicScheduleConstraint.java 8c64023fd01bcf858218e322f020aceff3661d98 GREEN
ConstraintDefinitionUtils.java a51705fb421fd2d1d3c2a9b74a055947f7e70e98 GREEN
BasicScheduleConstraint.java 87edb7bb45fa9b347f34b32c816e23189a697576 GREEN
ConstraintDefinitionUtils.java 8a709a9cd10edd36d1ac3ed0ded0c938aa010f12 GREEN
ConstraintTransformationAdapter.java 8806164d71491c7d1af665990dd154f2275cad8c GREEN
DSMLTransformationService.java 2344a468547413121ba43a12556c38812a63de5f GREEN
DSMLtoSMTTransformator.java 2a9b4efa2210a4a1da5c2b4328fd99cfe928028b GREEN
DefaultExpressionTransformator.java 47e3c00647a2a9845d1c0785668f6270cf06517e GREEN
DSMLTransformationService.java 2c19395bffa10cdaf2e7f38fdb592254289e659c GREEN
DSMLtoSMTTransformator.java c4f76eef0fece9eb87f4588f37ded3183f66ef4b GREEN
DefaultExpressionTransformator.java 9f572be21d1d96bc3d7604695678e57035a1b82e GREEN
DeploScheduleRun.java 2b07bd6b40cf4ce2eabc12198f6db3b9655bed25 GREEN
DeploymentRun.java 4b2d0a6d64bb5a6efabc2ee9bf933cc523843ac8 GREEN
EnergyConstraintDefinition.java 5bbe0c08a29dcc4ec0e4006aaf3fd221a5ecab09 GREEN
ExpressionTransformator.java 2823e34c90a86e11d7ad76e3ddefca9afde155d9 GREEN
IDSMLTransformationService.java eed05093deee8c85c8fc710159d7aa6fdb71c221 GREEN
EnergyConstraintDefinition.java cc18ecec975ce706ebcb83e282c9a17fe4608596 GREEN
ExpressionTransformator.java 81dfc30221e519aa8175693353ace8992687327f GREEN
IDSMLTransformationService.java 4c5bd9a06d74e31823bd8ef586687cbb344291e0 GREEN
NonQuantifiedExpressionTransformator.java 9ee437aeaf518d94b81e34a275cd01b87cfca1bf GREEN
QuantifiedExpressionTransformator.java 01e7162b24d16adb23f646cf02340879e8a18205 GREEN
SMTTransformationUtils.java c4900a17c5a708a628e4267b35652e2cfd72c78d GREEN
SMTTransformationUtils.java 376da0f5dafb350b49004c7d75fb8858b53d3b7d GREEN
ScheduleRun.java 43d869a9adfbebe34c34f1ebb0bc8e0600f45b9d GREEN
SolverRun.java 254914496ebfba7190ff6aa2a249a906d21afca3 GREEN
TimingConstraintDefinition.java 812f435186ad4e83436e7d0b21f54979852046fc GREEN
TimingConstraintDefinition.java c6cdc7b0d27c401cadbfa73c304cf43e56f26be7 GREEN
......@@ -64,7 +64,7 @@ import java.util.List;
import java.util.Optional;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ArithmeticLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ModelElementPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ArithmeticPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.Plus;
import org.fortiss.af3.exploration.dseml.model.booleanp.And;
import org.fortiss.af3.exploration.dseml.model.booleanp.ForAll;
......@@ -190,7 +190,8 @@ public class BasicDeploScheduleConstraint {
createSet(rsAllocSet, "aResourceAllocations", ResourceAllocation.class);
set.getEntries().addAll(rsAllocSet.getEntries());
ModelElementPropertyLiteral startSet1 = createStartTimeLiteral(set);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet1 =
createStartTimeLiteral(set);
ArithmeticLiteral literal = createArithmeticLiteral(BigDecimal.ZERO);
GreaterEqual gEquals = createGreaterEqual(startSet1, literal);
ForAll forAll1 = generateForAll(set, gEquals, true);
......@@ -376,16 +377,22 @@ public class BasicDeploScheduleConstraint {
// [(start(s1)+duration(s1) <= start(s2)) ||
// (start(s2)+duration(s2) <= start(s1))]
ModelElementPropertyLiteral startSet1 = createStartTimeLiteral(raSet1);
ModelElementPropertyLiteral startSet2 = createStartTimeLiteral(raSet2);
ModelElementPropertyLiteral durationSet1 = createDurationLiteral(raSet1);
ModelElementPropertyLiteral durationSet2 = createDurationLiteral(raSet2);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet1 =
createStartTimeLiteral(raSet1);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet2 =
createStartTimeLiteral(raSet2);
ArithmeticPropertyLiteral<ResourceAllocation, Number> durationSet1 =
createDurationLiteral(raSet1);
ArithmeticPropertyLiteral<ResourceAllocation, Number> durationSet2 =
createDurationLiteral(raSet2);
Plus endSet1 = createPlus(startSet1, durationSet1);
Plus endSet2 = createPlus(startSet2, durationSet2);
ModelElementPropertyLiteral startSet11 = createStartTimeLiteral(raSet1);
ModelElementPropertyLiteral startSet22 = createStartTimeLiteral(raSet2);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet11 =
createStartTimeLiteral(raSet1);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet22 =
createStartTimeLiteral(raSet2);
LessEqual cond1 = createLessEqual(endSet1, startSet22);
LessEqual cond2 = createLessEqual(endSet2, startSet11);
......@@ -456,14 +463,20 @@ public class BasicDeploScheduleConstraint {
// [(start(ra1)+duration(ra1) <= start(ra2)) ||
// (start(ra2)+duration(ra2) <= start(ra1))]
ModelElementPropertyLiteral startSet1 = createStartTimeLiteral(raSet1);
ModelElementPropertyLiteral startSet2 = createStartTimeLiteral(raSet2);
ModelElementPropertyLiteral durationSet1 = createDurationLiteral(raSet1);
ModelElementPropertyLiteral durationSet2 = createDurationLiteral(raSet2);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet1 =
createStartTimeLiteral(raSet1);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet2 =
createStartTimeLiteral(raSet2);
ArithmeticPropertyLiteral<ResourceAllocation, Number> durationSet1 =
createDurationLiteral(raSet1);
ArithmeticPropertyLiteral<ResourceAllocation, Number> durationSet2 =
createDurationLiteral(raSet2);
Plus endSet1 = createPlus(startSet1, durationSet1);
Plus endSet2 = createPlus(startSet2, durationSet2);
ModelElementPropertyLiteral startSet11 = createStartTimeLiteral(raSet1);
ModelElementPropertyLiteral startSet22 = createStartTimeLiteral(raSet2);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet11 =
createStartTimeLiteral(raSet1);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet22 =
createStartTimeLiteral(raSet2);
LessEqual cond1 = createLessEqual(endSet1, startSet22);
LessEqual cond2 = createLessEqual(endSet2, startSet11);
Or conclusion = createOr(cond1, cond2);
......@@ -510,7 +523,8 @@ public class BasicDeploScheduleConstraint {
Set<ResourceAllocation> oneElementSet = createSet(resAllocSS,
currentRA.getName() + "_set", ResourceAllocation.class);
oneElementSet.getEntries().add(currentRA);
ModelElementPropertyLiteral duration = createDurationLiteral(oneElementSet);
ArithmeticPropertyLiteral<ResourceAllocation, Number> duration =
createDurationLiteral(oneElementSet);
ArithmeticLiteral literal = createArithmeticLiteral(currentRA.getDuration());
Equal equals = createEquals(literal, duration);
ForAll formula = generateForAll(oneElementSet, equals, true);
......@@ -547,7 +561,8 @@ public class BasicDeploScheduleConstraint {
ModelElementLiteral r = createModelElementLiteral(routeSet);
Allocation allocation = createAllocation(s, r);
ModelElementPropertyLiteral durationLit = createDurationLiteral(ra);
ArithmeticPropertyLiteral<ResourceAllocation, Number> durationLit =
createDurationLiteral(ra);
Equal duration;
ArithmeticLiteral value;
......@@ -633,7 +648,8 @@ public class BasicDeploScheduleConstraint {
// (duration(ra) ==
// (wcet(task,ecu,freq))
ModelElementPropertyLiteral duration = createDurationLiteral(ra);
ArithmeticPropertyLiteral<ResourceAllocation, Number> duration =
createDurationLiteral(ra);
BigDecimal value = getWcet(taskWcetTable, (Task)modelElement, ecu, frequency);
int valueInt = value.intValue();
ArithmeticLiteral valueLiteral = createArithmeticLiteral(new BigDecimal(valueInt));
......
......@@ -44,8 +44,8 @@ import java.util.HashSet;
import java.util.List;
import org.eclipse.emf.common.util.EList;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ArithmeticPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.IArithmeticExpression;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ModelElementPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.Plus;
import org.fortiss.af3.exploration.dseml.model.booleanp.And;
import org.fortiss.af3.exploration.dseml.model.booleanp.ForAll;
......@@ -206,8 +206,10 @@ public class BasicScheduleConstraint {
"sourceResourceAllocation", ResourceAllocation.class);
source.getEntries().add(resourceAllocationSource);
ModelElementPropertyLiteral destStart = createStartTimeLiteral(dest);
ModelElementPropertyLiteral sourceStart = createStartTimeLiteral(source);
ArithmeticPropertyLiteral<ResourceAllocation, Number> destStart =
createStartTimeLiteral(dest);
ArithmeticPropertyLiteral<ResourceAllocation, Number> sourceStart =
createStartTimeLiteral(source);
ForAll formula;
LessEqual lessEqual;
......@@ -215,7 +217,8 @@ public class BasicScheduleConstraint {
if(!isStronglyCausal(sourceTask, co2taSet)) {
// formula to be added:
// source.start + source.duration <= dest.start
ModelElementPropertyLiteral sourceDuration = createDurationLiteral(source);
ArithmeticPropertyLiteral<ResourceAllocation, Number> sourceDuration =
createDurationLiteral(source);
Plus sourceEnd = createPlus(sourceStart, sourceDuration);
lessEqual = createLessEqual(sourceEnd, destStart);
}
......@@ -260,16 +263,22 @@ public class BasicScheduleConstraint {
// TODO(#3474, AD): Add some pseudo-code in a comment that describes the code below.
// Otherwise, the code cannot be understood without a lot of effort.
ModelElementPropertyLiteral startSet1 = createStartTimeLiteral(raSet1);
ModelElementPropertyLiteral startSet2 = createStartTimeLiteral(raSet2);
ModelElementPropertyLiteral durationSet1 = createDurationLiteral(raSet1);
ModelElementPropertyLiteral durationSet2 = createDurationLiteral(raSet2);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet1 =
createStartTimeLiteral(raSet1);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet2 =
createStartTimeLiteral(raSet2);
ArithmeticPropertyLiteral<ResourceAllocation, Number> durationSet1 =
createDurationLiteral(raSet1);
ArithmeticPropertyLiteral<ResourceAllocation, Number> durationSet2 =
createDurationLiteral(raSet2);
Plus endSet1 = createPlus(startSet1, durationSet1);
Plus endSet2 = createPlus(startSet2, durationSet2);
ModelElementPropertyLiteral startSet11 = createStartTimeLiteral(raSet1);
ModelElementPropertyLiteral startSet22 = createStartTimeLiteral(raSet2);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet11 =
createStartTimeLiteral(raSet1);
ArithmeticPropertyLiteral<ResourceAllocation, Number> startSet22 =
createStartTimeLiteral(raSet2);
LessEqual cond1 = createLessEqual(endSet1, startSet22);
LessEqual cond2 = createLessEqual(endSet2, startSet11);
......@@ -355,15 +364,15 @@ public class BasicScheduleConstraint {
// Skip if both tasks are deployed to the same ECU or both are strongly causal
continue;
}
ForAll sourceTaskForAll = createForAll();
sourceTaskForAll.setUnfold(true);
Set<ResourceAllocation> sourceTaskSet = createSet(rsAllocSet,
"sourceTaskResourceAllocation", ResourceAllocation.class);
sourceTaskSet.getEntries().add(sourceTaskRa);
sourceTaskForAll.setSet(sourceTaskSet.getCastedSet(IModelElement.class));
ModelElementPropertyLiteral sourceTaskStart = createStartTimeLiteral(sourceTaskSet);
ModelElementPropertyLiteral sourceTaskDuration =
ArithmeticPropertyLiteral<ResourceAllocation, Number> sourceTaskStart =
createStartTimeLiteral(sourceTaskSet);
ArithmeticPropertyLiteral<ResourceAllocation, Number> sourceTaskDuration =
createDurationLiteral(sourceTaskSet);
Plus sourceTaskEnd = createPlus(sourceTaskStart, sourceTaskDuration);
IArithmeticExpression lastEnd = sourceTaskEnd;
......@@ -390,7 +399,7 @@ public class BasicScheduleConstraint {
"destinationTaskResourceAllocation", ResourceAllocation.class);
destTaskSet.getEntries().add(targetTaskRa);
destTaskForAll.setSet(destTaskSet.getCastedSet(IModelElement.class));
ModelElementPropertyLiteral destTaskStart =
ArithmeticPropertyLiteral<ResourceAllocation, Number> destTaskStart =
createStartTimeLiteral(destTaskSet);
LessEqual lessEqualDest = createLessEqual(lastEnd, destTaskStart);
......@@ -413,7 +422,8 @@ public class BasicScheduleConstraint {
"signalResourceAllocation" + i++, ResourceAllocation.class);
setSignal.getEntries().add(sourceTaskPortRa);
forAllSignal.setSet(setSignal.getCastedSet(IModelElement.class));
ModelElementPropertyLiteral signalStart = createStartTimeLiteral(setSignal);
ArithmeticPropertyLiteral<ResourceAllocation, Number> signalStart =
createStartTimeLiteral(setSignal);
IBooleanExpression lessEqual;
// No constraint on the first communication segment (i.e., 2nd segment since
// the first one references the sender ECU) if sender is strongly causal.
......@@ -425,10 +435,10 @@ public class BasicScheduleConstraint {
}
lessEqualList.add(lessEqual);
ModelElementPropertyLiteral signalDuration =
ArithmeticPropertyLiteral<ResourceAllocation, Number> signalDuration =
createDurationLiteral(setSignal);
// Need another copy of "signal start" to work around containment problems
ModelElementPropertyLiteral signalStart2 =
ArithmeticPropertyLiteral<ResourceAllocation, Number> signalStart2 =
createStartTimeLiteral(setSignal);
Plus signalEnd = createPlus(signalStart2, signalDuration);
lastEnd = signalEnd;
......
......@@ -18,10 +18,13 @@ package org.fortiss.af3.exploration.smt.modeltransformation;
import static java.math.BigDecimal.ZERO;
import static java.util.stream.Collectors.toSet;
import static org.fortiss.af3.exploration.smt.modeltransformation.EnergyConstraintDefinition.STD_FREQ;
import static org.fortiss.af3.exploration.smt.modeltransformation.SMTTransformationUtils.DURATION_IDENTIFIER;
import static org.fortiss.af3.exploration.smt.modeltransformation.SMTTransformationUtils.START_TIME_IDENTIFIER;
import static org.fortiss.af3.exploration.smt.util.AllocationToSchedule.createResourceAllocation;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createAllocation;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createAnnotationArithPropLit;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createArithmeticPropertyLiteral;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createBooleanLiteral;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createElementPropertyLiteral;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createEquals;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createForAll;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createIsTask;
......@@ -44,8 +47,8 @@ import java.util.List;
import org.eclipse.emf.common.util.EList;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ArithmeticPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.IArithmeticExpression;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ModelElementPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.booleanp.BooleanLiteral;
import org.fortiss.af3.exploration.dseml.model.booleanp.ForAll;
import org.fortiss.af3.exploration.dseml.model.booleanp.IBooleanExpression;
......@@ -61,8 +64,6 @@ import org.fortiss.af3.exploration.dseml.model.function.ScheduledSignal;
import org.fortiss.af3.exploration.dseml.model.function.ScheduledTask;
import org.fortiss.af3.exploration.dseml.model.function.Start;
import org.fortiss.af3.exploration.dseml.model.function.StronglyCausal;
import org.fortiss.af3.exploration.smt.model.DurationDummy;
import org.fortiss.af3.exploration.smt.model.StartTimeDummy;
import org.fortiss.af3.exploration.smt.model.dseml.DsemlFactory;
import org.fortiss.af3.exploration.smt.model.dseml.FrequencyAssigned;
import org.fortiss.af3.platform.model.ExecutionUnit;
......@@ -166,37 +167,30 @@ public class ConstraintDefinitionUtils {
}
/** For the given set of {@link ResourceAllocation}, creates a corresponding start time set. */
public static ModelElementPropertyLiteral createStartTimeLiteral(Set<ResourceAllocation> set) {
// TODO (#3472, SB, 9): Explain what is a StartTimeDummy, and why creation of dedicated
// copies is needed.
return createElementPropertyLiteral(set.getCastedSet(IModelElement.class),
StartTimeDummy.class);
public static ArithmeticPropertyLiteral<ResourceAllocation, Number>
createStartTimeLiteral(Set<ResourceAllocation> set) {
// Create a arithmetic property literal representing an arithmetic decision variable. Its
// name is used to create a "floating" function in Z3 and the extraction of the assigned
// values from the resulting model.
return createArithmeticPropertyLiteral(set, null, START_TIME_IDENTIFIER);
}
/** For the given set of {@link ResourceAllocation}, creates a corresponding duration set. */
public static ModelElementPropertyLiteral createDurationLiteral(Set<ResourceAllocation> set) {
// TODO (#3472 SB, 9): Explain what is a DurationDummy, and why creation of dedicated copies
// is needed.
return createElementPropertyLiteral(set.getCastedSet(IModelElement.class),
DurationDummy.class);
}
/** For the given set of {@link ResourceAllocation}, creates a corresponding duration set. */
public static ModelElementPropertyLiteral createTaskDurationLiteral(Set<Task> set) {
// TODO (#3472 SB, 9): Explain what is a DurationDummy, and why creation of dedicated copies
// is needed.
return createElementPropertyLiteral(set.getCastedSet(IModelElement.class),
DurationDummy.class);
public static ArithmeticPropertyLiteral<ResourceAllocation, Number>
createDurationLiteral(Set<ResourceAllocation> set) {
// Create a arithmetic property literal representing an arithmetic decision variable. Its
// name is used to create a "floating" function in Z3 and the extraction of the assigned
// values from the resulting model.
return createArithmeticPropertyLiteral(set, null, DURATION_IDENTIFIER);
}
/**
* For the given set of {@link ExecutionUnit}s, creates a corresponding {@link PowerConsumption}
* literal.
*/
public static ModelElementPropertyLiteral
public static ArithmeticPropertyLiteral<ExecutionUnit, Number>
createPowerConsumptionLiteral(Set<ExecutionUnit> set) {
return createElementPropertyLiteral(set.getCastedSet(IModelElement.class),
PowerConsumption.class);
return createAnnotationArithPropLit(set, PowerConsumption.class);
}
/**
......@@ -248,8 +242,10 @@ public class ConstraintDefinitionUtils {
return createStartTimeLiteral(set);
}
if((event instanceof TaskTerminateEvent) || (event instanceof SignalReceiveEvent)) {
ModelElementPropertyLiteral start = createStartTimeLiteral(set);
ModelElementPropertyLiteral duration = createDurationLiteral(set);
ArithmeticPropertyLiteral<ResourceAllocation, Number> start =
createStartTimeLiteral(set);
ArithmeticPropertyLiteral<ResourceAllocation, Number> duration =
createDurationLiteral(set);
return createPlus(start, duration);
}
return null;
......
......@@ -21,21 +21,17 @@ import static com.microsoft.z3.Z3javaAPIWrapper.createSymbol;
import static org.fortiss.af3.exploration.smt.modeltransformation.SMTTransformationUtils.createSymbol;
import static org.fortiss.af3.exploration.smt.modeltransformation.SMTTransformationUtils.createUniqueASCIIModelName;
import static org.fortiss.af3.exploration.smt.modeltransformation.SMTTransformationUtils.getFunctionName;
import static org.fortiss.tooling.common.util.LambdaUtils.filter;
import static org.fortiss.tooling.common.util.LambdaUtils.getFirst;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Optional;
import java.util.function.Predicate;
import java.util.stream.Stream;
import org.eclipse.emf.common.util.EList;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ModelElementPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ArithmeticPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.expression.IExpression;
import org.fortiss.af3.exploration.dseml.model.expression.Set;
import org.fortiss.af3.exploration.dseml.model.expression.SuperSet;
......@@ -49,19 +45,14 @@ import org.fortiss.af3.exploration.dseml.model.function.StronglyCausal;
import org.fortiss.af3.exploration.dseml.model.function.Uses;
import org.fortiss.af3.exploration.dseml.model.function.Weight;
import org.fortiss.af3.exploration.model.SuperSetMap;
import org.fortiss.af3.exploration.smt.model.DurationDummy;
import org.fortiss.af3.exploration.smt.model.StartTimeDummy;
import org.fortiss.af3.exploration.smt.model.dseml.FrequencyAssigned;
import org.fortiss.af3.platform.model.ExecutionUnit;
import org.fortiss.af3.platform.model.Route;
import org.fortiss.af3.platform.model.TransmissionUnit;
import org.fortiss.af3.safety.model.annotation.SafetyIntegrityLevel;
import org.fortiss.af3.schedule.model.ResourceAllocation;
import org.fortiss.af3.task.model.Signal;
import org.fortiss.af3.task.model.Task;
import org.fortiss.af3.task.model.allocation.ComponentToTaskAllocationEntry;
import org.fortiss.af3.task.model.allocation.SignalToRouteAllocationEntry;
import org.fortiss.tooling.base.model.element.IAnnotatedSpecification;
import org.fortiss.tooling.base.model.element.IModelElement;
import com.microsoft.z3.ArithExpr;
......@@ -91,9 +82,6 @@ public class DSMLTransformationService implements IDSMLTransformationService {
/** Mapping of leftSort to rightSort to the respective allocation {@link FuncDecl}. */
private Map<EnumSort, Map<EnumSort, FuncDecl>> allocations = new HashMap<>();
/** The current {@link SuperSetMap}. */
private SuperSetMap superSets;
/** The current Z3 {@link Context}. */
private Context context;
......@@ -102,7 +90,6 @@ public class DSMLTransformationService implements IDSMLTransformationService {
/** Constructor */
public DSMLTransformationService(SuperSetMap superSets, Context context) {
this.superSets = superSets;
this.context = context;
existingSorts.clear();
existingSymbols.clear();
......@@ -170,15 +157,6 @@ public class DSMLTransformationService implements IDSMLTransformationService {
addExistingSymbol(sort, elementOfSort);
}
/** {@inheritDoc} */
@Override
public ArithExpr getZ3Function(Class<? extends IAnnotatedSpecification> annot,
IModelElement modelElement) {
String name = getFunctionName(annot);
EnumSort sort = searchForReferringZ3Set(modelElement);
return getZ3FunctionForModelElement(context, modelElement, name, sort);
}
/**
* Returns the Z3 function for the given model element of type sort with the given function
* name.
......@@ -196,10 +174,11 @@ public class DSMLTransformationService implements IDSMLTransformationService {
/** {@inheritDoc} */
@Override
public ArithExpr getZ3Function(ModelElementPropertyLiteral arithExpr, IModelElement model) {
public ArithExpr getZ3Function(
ArithmeticPropertyLiteral<? extends IModelElement, Number> arithExpr,
IModelElement model) {
String name = getFunctionName(arithExpr);
EnumSort sort = getSort(model);
return getZ3FunctionForModelElement(context, model, name, sort);
return getZ3FunctionForModelElement(context, model, name, getSort(model));
}
/** {@inheritDoc} */
......@@ -377,17 +356,6 @@ public class DSMLTransformationService implements IDSMLTransformationService {
return sort;
}
/** Searches for the referring EnumSort for the given {@link Set} reference. */
private EnumSort searchForReferringZ3Set(IModelElement modelElement) {
// search for the set containing all elements of setReference
for(Entry<Set<? extends IModelElement>, EnumSort> e : existingSorts.entrySet()) {
if(e.getKey().getEntries().contains(modelElement)) {
return e.getValue();
}
}
return null;
}
/** {@inheritDoc} */
@Override
public Expr getZ3Function(Start start) {
......@@ -550,32 +518,6 @@ public class DSMLTransformationService implements IDSMLTransformationService {
return null;
}
/** {@inheritDoc} */
@Override
public IModelElement getParameterProvider(IModelElement modelElement,
Class<? extends IAnnotatedSpecification> type) {
// Ignore dummy schedule elements see #3472
if(type.equals(StartTimeDummy.class) || type.equals(DurationDummy.class)) {
return null;
}
// The Safety Integrity Level associated with a task is a property of the respective
// component, not the task itself.
if(modelElement instanceof Task && type.equals(SafetyIntegrityLevel.class)) {
SuperSet<ComponentToTaskAllocationEntry> ca2taSet =
superSets.get(ComponentToTaskAllocationEntry.class);
// Returns the allocated component to this task. Relies on the assumption that there is
// a 1:1 mapping between components and tasks.
Optional<ComponentToTaskAllocationEntry> alloc = getFirst(
filter(ca2taSet.getEntries(), e -> e.getTargetElement() == modelElement));
return alloc.isPresent()
? (Component)getFirst(alloc.get().getSourceElements()).orElse(null) : null;
}
return modelElement;
}
/** Adds an {@link EnumSort} referring to a given {@link Set} of {@link IModelElement}s. */
private <T extends IModelElement> void addExistingSort(Set<T> set, EnumSort sort) {
existingSorts.put(set, sort);
......
......@@ -38,10 +38,10 @@ import java.util.Map;
import javax.activation.UnsupportedDataTypeException;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ArithmeticLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ArithmeticPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.Div;
import org.fortiss.af3.exploration.dseml.model.arithmetic.IArithmeticExpression;
import org.fortiss.af3.exploration.dseml.model.arithmetic.Minus;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ModelElementPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.Mul;
import org.fortiss.af3.exploration.dseml.model.arithmetic.Plus;
import org.fortiss.af3.exploration.dseml.model.booleanp.And;
......@@ -132,8 +132,8 @@ public class DefaultExpressionTransformator extends ExpressionTransformator {
} else if(expression instanceof Mul) {
return createMultiplication(context, (ArithExpr)left, (ArithExpr)right);
}
} else if(expression instanceof ModelElementPropertyLiteral) {
return getZ3Function((ModelElementPropertyLiteral)expression, modelElements);
} else if(expression instanceof ArithmeticPropertyLiteral) {
return getZ3Function((ArithmeticPropertyLiteral<?, ?>)expression, modelElements);
} else if(expression instanceof ArithmeticLiteral) {
final String string = ((ArithmeticLiteral)expression).getValue().toString();
return createReal(context, string);
......@@ -142,13 +142,14 @@ public class DefaultExpressionTransformator extends ExpressionTransformator {
expression.getClass().getSimpleName() + "' implemented.");
}
/** Returns an {@link ArithExpr} for the given {@link ModelElementPropertyLiteral}. */
private ArithExpr getZ3Function(ModelElementPropertyLiteral arithExpr,
/** Returns an {@link ArithExpr} for the given {@link ArithmeticPropertyLiteral}. */
private ArithExpr getZ3Function(
ArithmeticPropertyLiteral<? extends IModelElement, ? extends Number> arithExpr,
Map<Set<IModelElement>, IModelElement> modelElements)
throws UnsupportedDataTypeException, Z3Exception {
String name = getFunctionName(arithExpr);
Set<IModelElement> setReference = arithExpr.getSetReference();
Set<IModelElement> superSetReference = setReference.getSuperSetReference();
Set<? extends IModelElement> setReference = arithExpr.getSetReference();
Set<? extends IModelElement> superSetReference = setReference.getSuperSetReference();
EnumSort sort = transformationService.getExistingSorts().get(superSetReference);
FuncDecl function = createFunction(context, name, sort, context.getIntSort());
......
......@@ -44,8 +44,8 @@ import java.util.List;
import org.eclipse.emf.common.util.EList;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ArithmeticLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ArithmeticPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.Maximum;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ModelElementPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.arithmetic.Mul;
import org.fortiss.af3.exploration.dseml.model.arithmetic.Plus;
import org.fortiss.af3.exploration.dseml.model.arithmetic.Sum;
......@@ -135,7 +135,8 @@ public class EnergyConstraintDefinition {
Mul dynamicPowerConsumption = createMul(frequencyEcu, frequencyEcuCopy);
// Sum_{ra \in ResourceAllocation | scheduledTask(ra)=t && isTask(ra)} (duration(ra))
ModelElementPropertyLiteral duration = createDurationLiteral(raSet);
ArithmeticPropertyLiteral<ResourceAllocation, Number> duration =
createDurationLiteral(raSet);
ScheduledTask elem = createScheduledTask(raSet, taskSet);