Commit 60b8a90a authored by Alexander Diewald's avatar Alexander Diewald

Merge remote-tracking branch 'origin/master' into 3994

Conflicts:
	org.fortiss.af3.exploration.ui/src/org/fortiss/af3/exploration/ui/menu/.ratings
	org.fortiss.af3.exploration.ui/src/org/fortiss/af3/exploration/ui/perspective/generic/.ratings
	org.fortiss.af3.exploration.ui/src/org/fortiss/af3/exploration/ui/perspective/navigator/.ratings
	org.fortiss.af3.exploration/src/org/fortiss/af3/exploration/lang/.ratings
	org.fortiss.af3.exploration/src/org/fortiss/af3/exploration/lang/ExplorationExpressionDeploymentValidator.java
	org.fortiss.af3.exploration/src/org/fortiss/af3/exploration/util/.ratings
Signed-off-by: Alexander Diewald's avatarAlexander Diewald <diewald@fortiss.org>
parents cefe2f60 7f59418c
......@@ -16,9 +16,6 @@ Require-Bundle: org.fortiss.af3.exploration,
org.fortiss.af3.safety;visibility:=reexport,
org.fortiss.tooling.kernel.ui
Export-Package: org.fortiss.af3.exploration.smt.backend,
org.fortiss.af3.exploration.smt.model,
org.fortiss.af3.exploration.smt.model.impl,
org.fortiss.af3.exploration.smt.model.util,
org.fortiss.af3.exploration.smt.modeltransformation,
org.fortiss.af3.exploration.smt.util,
test.org.fortiss.af3.exploration.smt
model.ecore 3159422b58b66acc4c36ccc8e318a2b9b1773da5 GREEN
model.ecore 3e1b36f950369b789a95159d87158218d3628a41 GREEN
......@@ -3,7 +3,7 @@
xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" name="model" nsURI="http://www.fortiss.org/af3/exploration/smt" nsPrefix="org-fortiss-af3-exploration-smt">
<eClassifiers xsi:type="ecore:EClass" name="SMTConstraint">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
<details key="documentation" value="ExplorationConstraint for translation into SMT. If unfoldQuantifier is true, any quantifier will be unfolded."/>
<details key="documentation" value="@deprecated Use {@link org.fortiss.af3.exploration.model.ExplorationConstraint} instead."/>
</eAnnotations>
<eGenericSuperTypes eClassifier="ecore:EClass platform:/resource/org.fortiss.af3.exploration/model/exploration.ecore#//ExplorationConstraint">
<eTypeArguments eClassifier="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBooleanObject"/>
......@@ -12,7 +12,7 @@
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="SMTObjective">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
<details key="documentation" value="ExplorationObjective for translation into SMT. Additional needed SMTConstraints may be contained."/>
<details key="documentation" value="@deprecated Use {@link org.fortiss.af3.exploration.model.ExplorationObjective} instead."/>
</eAnnotations>
<eStructuralFeatures xsi:type="ecore:EReference" name="constraints" upperBound="-1"
eType="#//SMTConstraint" containment="true">
......@@ -25,9 +25,9 @@
</eGenericSuperTypes>
<eGenericSuperTypes eClassifier="#//CustomDimension"/>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="CustomDimension" eSuperTypes="platform:/resource/org.fortiss.af3.exploration/model/exploration.ecore#//IProblemDimension">
<eClassifiers xsi:type="ecore:EClass" name="CustomDimension">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
<details key="documentation" value="Custom dimension whose name is determined by the dimension string."/>
<details key="documentation" value="@deprecated See the subclasses of {@link org.fortiss.af3.exploration.model.IProblemDimension} for an alternative."/>
</eAnnotations>
<eStructuralFeatures xsi:type="ecore:EAttribute" name="dimension" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"
defaultValueLiteral="category">
......
......@@ -11,4 +11,13 @@
class="org.fortiss.af3.exploration.smt.model.AF3ExplorationSMTPackage"
genModel="model/model.genmodel"/>
</extension>
<extension
point="org.fortiss.tooling.kernel.migrationProvider">
<migrationProvider
migrationProvider="org.fortiss.af3.exploration.smt.migrate.SMTExplorationTargetMigrator">
<objectClass
objectClass="org.fortiss.af3.exploration.model.project.DSE">
</objectClass>
</migrationProvider>
</extension>
</plugin>
Z3Backend.java f9cb53217d533e7014cc32fceee9d6922d145f4e GREEN
Z3Backend.java 070f627218b36e50f61c56d850d0679e5a69d332 GREEN
......@@ -28,12 +28,12 @@ import java.util.Set;
import org.eclipse.core.runtime.IProgressMonitor;
import org.fortiss.af3.exploration.model.ExplorationSpecification;
import org.fortiss.af3.exploration.model.ExplorationTarget;
import org.fortiss.af3.exploration.model.IExplorationConstraint;
import org.fortiss.af3.exploration.model.IExplorationTarget;
import org.fortiss.af3.exploration.model.SuperSetMap;
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.BasicScheduleConstraint;
import org.fortiss.af3.exploration.smt.modeltransformation.DeploScheduleRun;
import org.fortiss.af3.exploration.smt.modeltransformation.DeploymentRun;
......@@ -84,10 +84,10 @@ public class Z3Backend implements IDSEBackend {
Set<Class<? extends IModelElement>> solutionTypes, IProgressMonitor monitor,
int timeoutMS) throws Exception {
// For SMT, we must add constraints in the correct order: user last.
List<ExplorationTarget<?>> inputTargets = new ArrayList<>(spec.getTargets());
List<IExplorationTarget<?>> inputTargets = new ArrayList<>(spec.getTargets());
spec.getTargets().clear();
List<ExplorationTarget<?>> basicConstraints = new ArrayList<>();
List<IExplorationTarget<?>> basicConstraints = new ArrayList<>();
SuperSetMap superSets = spec.getSearchSpace();
SolverRun solverRun;
......@@ -99,7 +99,7 @@ public class Z3Backend implements IDSEBackend {
if(solutionTypes.contains(Schedule.class)) {
// Case deployment+schedule run
// Add SMT-specific constraints to define the deployment+schedule problem.
List<SMTConstraint> basicDeploScheduleConstraints =
List<IExplorationConstraint<?>> basicDeploScheduleConstraints =
generateDeploScheduleConstraints(superSets.get(ResourceAllocation.class),
superSets.get(Task.class), superSets.get(Signal.class),
superSets.get(ExecutionUnit.class), superSets.get(Route.class),
......@@ -123,14 +123,15 @@ public class Z3Backend implements IDSEBackend {
} else {
// Case pure schedule run
// Add SMT-specific constraints to define the deployment+schedule problem.
List<SMTConstraint> basicDeploScheduleConstraints = generateDeploScheduleConstraints(
superSets.get(ResourceAllocation.class), superSets.get(Task.class),
superSets.get(Signal.class), superSets.get(ExecutionUnit.class),
superSets.get(Route.class), superSets.get(ComponentToTaskAllocationEntry.class),
superSets.get(TaskWcetTable.class));
List<IExplorationConstraint<?>> basicDeploScheduleConstraints =
generateDeploScheduleConstraints(superSets.get(ResourceAllocation.class),
superSets.get(Task.class), superSets.get(Signal.class),
superSets.get(ExecutionUnit.class), superSets.get(Route.class),
superSets.get(ComponentToTaskAllocationEntry.class),
superSets.get(TaskWcetTable.class));
// Add SMT-specific constraints to define the schedule problem, in the case when a
// deployment is given
List<SMTConstraint> basicScheduleConstraints = BasicScheduleConstraint
List<IExplorationConstraint<?>> basicScheduleConstraints = BasicScheduleConstraint
.generatePureScheduleConstraints(superSets.get(ResourceAllocation.class),
superSets.get(Task.class), superSets.get(ExecutionUnit.class),
superSets.get(ComponentToTaskAllocationEntry.class),
......@@ -154,7 +155,7 @@ public class Z3Backend implements IDSEBackend {
// prints on screen the list of constraints for this run
int i = 1;
System.out.println("*** List of constraints ***");
for(ExplorationTarget<?> et : spec.getTargets()) {
for(IExplorationTarget<?> et : spec.getTargets()) {
System.out.println(" ExplorationTarget " + i + " : " + et);
System.out.println(et.getExpression());
i++;
......
SMTExplorationTargetMigrator.java 843c5e4b8ddb7ddb1ca6f670da6b3d3bb839fe88 GREEN
/*-------------------------------------------------------------------------+
| Copyright 2020 fortiss GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.migrate;
import static org.eclipse.emf.ecore.util.EcoreUtil.replace;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationConstraint;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationObjective;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createUserDefinedDimension;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getFirstChildWith;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.Map;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.xml.type.AnyType;
import org.fortiss.af3.exploration.model.ExplorationConstraint;
import org.fortiss.af3.exploration.model.ExplorationObjective;
import org.fortiss.af3.exploration.model.IExplorationTarget;
import org.fortiss.af3.exploration.model.project.DSE;
import org.fortiss.af3.exploration.model.project.RuleSet;
import org.fortiss.af3.exploration.model.solutions.ExplorationResult;
import org.fortiss.af3.exploration.model.solutions.SingleExplorationSolution;
import org.fortiss.af3.exploration.smt.model.CustomDimension;
import org.fortiss.af3.exploration.smt.model.SMTConstraint;
import org.fortiss.af3.exploration.smt.model.SMTObjective;
import org.fortiss.af3.project.model.FileProject;
import org.fortiss.tooling.kernel.extension.IMigrationProvider;
import org.fortiss.tooling.kernel.extension.data.ITopLevelElement;
/**
* Migrator for {@link SMTConstraint}s, {@link SMTObjective}s, and {@link CustomDimension}s to the
* commonized {@link IExplorationTarget}s.
*
* @author diewald
*/
@SuppressWarnings({"deprecation", "javadoc"})
public class SMTExplorationTargetMigrator implements IMigrationProvider {
/** {@inheritDoc} */
@Override
public boolean needMigration(ITopLevelElement modelElement,
Map<EObject, AnyType> unknownFeatures) {
EObject rootObj = modelElement.getRootModelElement();
if(!(rootObj instanceof FileProject)) {
return false;
}
FileProject fp = (FileProject)rootObj;
return getFirstChildWith(fp, c -> c instanceof SMTObjective || c instanceof SMTConstraint ||
c instanceof CustomDimension) != null;
}
/** {@inheritDoc} */
@SuppressWarnings("unchecked")
@Override
public Map<EObject, AnyType> migrate(ITopLevelElement modelElement,
Map<EObject, AnyType> unknownFeatures) {
EObject rootObj = modelElement.getRootModelElement();
if(!(rootObj instanceof FileProject)) {
return unknownFeatures;
}
FileProject fp = (FileProject)rootObj;
for(DSE dse : getChildrenWithType(fp, DSE.class)) {
Map<IExplorationTarget<?>, IExplorationTarget<?>> oldNewMap = new HashMap<>();
for(SMTObjective objective : getChildrenWithType(dse, SMTObjective.class)) {
ExplorationObjective<Double> newObjective = createExplorationObjective(Double.class,
createUserDefinedDimension(objective.getDimension()),
objective.getExpression(), objective.getName());
replace(objective, newObjective);
oldNewMap.put(objective, newObjective);
}
for(SMTConstraint constraint : getChildrenWithType(dse, SMTConstraint.class)) {
ExplorationConstraint<Boolean> newConstraint = createExplorationConstraint(
Boolean.class, createUserDefinedDimension(constraint.getDimension()),
constraint.getExpression(), constraint.getName(), constraint.isImplicit());
replace(constraint, newConstraint);
oldNewMap.put(constraint, newConstraint);
}
for(RuleSet ruleSet : getChildrenWithType(dse, RuleSet.class)) {
for(IExplorationTarget<?> target : new ArrayList<>(
ruleSet.getExplorationTargets())) {
ruleSet.getExplorationTargets().remove(target);
ruleSet.getExplorationTargets().add(oldNewMap.get(target));
}
}
for(SingleExplorationSolution sES : getChildrenWithType(dse,
SingleExplorationSolution.class)) {
for(IExplorationTarget<?> target : new ArrayList<>(sES.keySet())) {
IExplorationTarget<Object> castedTarget = (IExplorationTarget<Object>)target;
ExplorationResult<Object> result = (ExplorationResult<Object>)sES.get(target);
sES.removeKey(target);
sES.put((IExplorationTarget<Object>)oldNewMap.get(castedTarget), result);
}
}
}
return unknownFeatures;
}
}
BasicDeploScheduleConstraint.java 95c1a55dd30de0b62ab7da3aa7055ed446f8e01b GREEN
BasicDeploymentConstraint.java f66c59adfa5a1619db1f1178c95fe7a4b7930d6e GREEN
BasicScheduleConstraint.java 87edb7bb45fa9b347f34b32c816e23189a697576 GREEN
BasicDeploScheduleConstraint.java 76029b866e82f7fcbb78292e366a41d39ad86cdc GREEN
BasicDeploymentConstraint.java bd66d1e997b091ddd28423529de5a5c23af1bee9 GREEN
BasicScheduleConstraint.java 8b054b5ad961295b97936e26240eb33a10a1ee9a GREEN
ConstraintDefinitionUtils.java 8a709a9cd10edd36d1ac3ed0ded0c938aa010f12 GREEN
ConstraintTransformationAdapter.java 8806164d71491c7d1af665990dd154f2275cad8c GREEN
DSMLTransformationService.java 2c19395bffa10cdaf2e7f38fdb592254289e659c GREEN
DSMLtoSMTTransformator.java c4f76eef0fece9eb87f4588f37ded3183f66ef4b GREEN
DSMLtoSMTTransformator.java 32431ae9bcbca84d1c7cb9726f77af67019da250 GREEN
DefaultExpressionTransformator.java 9f572be21d1d96bc3d7604695678e57035a1b82e GREEN
DeploScheduleRun.java 2b07bd6b40cf4ce2eabc12198f6db3b9655bed25 GREEN
DeploymentRun.java 4b2d0a6d64bb5a6efabc2ee9bf933cc523843ac8 GREEN
......@@ -15,5 +15,5 @@ NonQuantifiedExpressionTransformator.java 9ee437aeaf518d94b81e34a275cd01b87cfca1
QuantifiedExpressionTransformator.java 01e7162b24d16adb23f646cf02340879e8a18205 GREEN
SMTTransformationUtils.java 376da0f5dafb350b49004c7d75fb8858b53d3b7d GREEN
ScheduleRun.java 43d869a9adfbebe34c34f1ebb0bc8e0600f45b9d GREEN
SolverRun.java 254914496ebfba7190ff6aa2a249a906d21afca3 GREEN
TimingConstraintDefinition.java c6cdc7b0d27c401cadbfa73c304cf43e56f26be7 GREEN
SolverRun.java be9794b2be0fd203a31435548abe9d9945bc2160 GREEN
TimingConstraintDefinition.java 92281277d99bb52b72c1cb898bba944b3b9a24f7 GREEN
......@@ -36,8 +36,6 @@ import static org.fortiss.af3.exploration.smt.modeltransformation.EnergyConstrai
import static org.fortiss.af3.exploration.smt.modeltransformation.EnergyConstraintDefinition.createMinimizeSumObjective;
import static org.fortiss.af3.exploration.smt.modeltransformation.EnergyConstraintDefinition.createTileFrequencyConstraints;
import static org.fortiss.af3.exploration.smt.modeltransformation.TimingConstraintDefinition.generateTimingConstraints;
import static org.fortiss.af3.exploration.smt.util.Z3ModelElementFactory.createSMTConstraint;
import static org.fortiss.af3.exploration.smt.util.Z3ModelElementFactory.createSMTObjective;
import static org.fortiss.af3.exploration.util.DSEProjectModelElementFactory.createRuleSet;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createAllocation;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createAnd;
......@@ -51,6 +49,11 @@ import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createNot
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createOr;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createPlus;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createSet;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createEnergyDimension;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationConstraint;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationObjective;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createTemporalDimension;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createUserDefinedDimension;
import static org.fortiss.af3.task.model.allocation.impl.TaskWcetTableStaticImpl.getWcet;
import static org.fortiss.tooling.base.utils.AnnotationUtils.getAnnotationValue;
import static org.fortiss.tooling.common.util.LambdaUtils.getFirst;
......@@ -84,12 +87,12 @@ import org.fortiss.af3.exploration.dseml.model.function.IsTask;
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.StronglyCausal;
import org.fortiss.af3.exploration.model.IExplorationConstraint;
import org.fortiss.af3.exploration.model.IExplorationObjective;
import org.fortiss.af3.exploration.model.SuperSetMap;
import org.fortiss.af3.exploration.model.project.DSE;
import org.fortiss.af3.exploration.model.project.ModelSnapshot;
import org.fortiss.af3.exploration.model.project.RuleSet;
import org.fortiss.af3.exploration.smt.model.SMTConstraint;
import org.fortiss.af3.exploration.smt.model.SMTObjective;
import org.fortiss.af3.exploration.smt.model.dseml.FrequencyAssigned;
import org.fortiss.af3.platform.model.ExecutionUnit;
import org.fortiss.af3.platform.model.Route;
......@@ -118,11 +121,11 @@ public class BasicDeploScheduleConstraint {
final static int BITS_IN_A_MEGABIT = 1000000;
/** Generates standard schedule constraints for a deployment+scheduling run. */
public static List<SMTConstraint> generateDeploScheduleConstraints(
public static List<IExplorationConstraint<?>> generateDeploScheduleConstraints(
SuperSet<ResourceAllocation> resAllocSS, SuperSet<Task> taskSS,
SuperSet<Signal> signalSS, SuperSet<ExecutionUnit> ecuSS, SuperSet<Route> routeSuperSet,
SuperSet<ComponentToTaskAllocationEntry> co2ta, SuperSet<TaskWcetTable> wcetTable) {
List<SMTConstraint> generatedConstraints = new ArrayList<>();
List<IExplorationConstraint<?>> generatedConstraints = new ArrayList<>();
List<IBooleanExpression> assertions = new ArrayList<>();
assertions = new ArrayList<>();
assertions.addAll(createStronglyCausalFunction(taskSS, co2ta));
......@@ -134,8 +137,10 @@ public class BasicDeploScheduleConstraint {
assertions.addAll(createFrequencyConstraints(ecuSS));
assertions.addAll(createTileFrequencyConstraints(ecuSS));
int i = 1;
for(IBooleanExpression a : assertions) {
SMTConstraint ts = createSMTConstraint("Implicit Schedule Constraint " + i++, a, true);
for(IBooleanExpression expr : assertions) {
IExplorationConstraint<?> ts =
createExplorationConstraint(Boolean.class, createUserDefinedDimension("unused"),
expr, "Implicit Schedule Constraint " + i++, true);
generatedConstraints.add(ts);
prepareUniqueID(ts, co2ta);
}
......@@ -149,9 +154,9 @@ public class BasicDeploScheduleConstraint {
* deployment+scheduling. Once that gets fixed, this method should be removed.
* Generates causality constraints for a deployment+scheduling run.
*/
public static List<SMTConstraint>
public static List<IExplorationConstraint<?>>
generateDeploScheduleSpecificConstraints(SuperSetMap superSets) {
List<SMTConstraint> generatedConstraints = new ArrayList<>();
List<IExplorationConstraint<?>> generatedConstraints = new ArrayList<>();
List<IBooleanExpression> assertions = new ArrayList<>();
SuperSet<ResourceAllocation> resAllocSS = superSets.get(ResourceAllocation.class);
SuperSet<Task> taskSS = superSets.get(Task.class);
......@@ -160,8 +165,9 @@ public class BasicDeploScheduleConstraint {
assertions.addAll(createECUNonOverlappingConstraints(resAllocSS, taskSS, ecuSS));
assertions.addAll(createRoutesNonOverlappingConstraints(resAllocSS));
int i = 1;
for(IBooleanExpression a : assertions) {
SMTConstraint ts = createSMTConstraint("Non-Overlapping Constraint " + i++, a, true);
for(IBooleanExpression expr : assertions) {
IExplorationConstraint<?> ts = createExplorationConstraint(Double.class,
createTemporalDimension(), expr, "Non-Overlapping Constraint " + i++, true);
generatedConstraints.add(ts);
prepareUniqueID(ts, superSets.get(ComponentToTaskAllocationEntry.class));
}
......@@ -169,8 +175,9 @@ public class BasicDeploScheduleConstraint {
assertions.clear();
assertions.addAll(createCausalityConstraints(resAllocSS, taskSS, signalSS, ecuSS));
i = 1;
for(IBooleanExpression a : assertions) {
SMTConstraint ts = createSMTConstraint("Causality Constraint " + i++, a, true);
for(IBooleanExpression expr : assertions) {
IExplorationConstraint<?> ts = createExplorationConstraint(Double.class,
createTemporalDimension(), expr, "Causality Constraint " + i++, true);
generatedConstraints.add(ts);
prepareUniqueID(ts, superSets.get(ComponentToTaskAllocationEntry.class));
}
......@@ -836,7 +843,8 @@ public class BasicDeploScheduleConstraint {
});
int i = 0;
for(IFunction o : objectives) {
SMTObjective oSmt = createSMTObjective("Latency Minimization Objective " + i++, o);
IExplorationObjective<?> oSmt = createExplorationObjective(Double.class,
createTemporalDimension(), o, "Latency Minimization Objective " + i++);
rs.getExplorationTargets().add(oSmt);
prepareUniqueID(oSmt, dse);
}
......@@ -858,7 +866,8 @@ public class BasicDeploScheduleConstraint {
});
int i = 0;
for(IFunction o : objectives) {
SMTObjective oSmt = createSMTObjective("Energy Consumption Objective " + i++, o);
IExplorationObjective<?> oSmt = createExplorationObjective(Double.class,
createEnergyDimension(), o, "Energy Consumption Objective " + i++);
rs.getExplorationTargets().add(oSmt);
prepareUniqueID(oSmt, dse);
}
......
......@@ -15,7 +15,6 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.modeltransformation;
import static org.fortiss.af3.exploration.smt.util.Z3ModelElementFactory.createSMTConstraint;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createAllocation;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createAnd;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createEquals;
......@@ -23,6 +22,9 @@ import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createFor
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createImplies;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createModelElementLiteral;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createSet;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationConstraint;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createResourceDimension;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createTemporalDimension;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
import java.util.ArrayList;
......@@ -43,9 +45,9 @@ import org.fortiss.af3.exploration.dseml.model.expression.SuperSet;
import org.fortiss.af3.exploration.dseml.model.function.End;
import org.fortiss.af3.exploration.dseml.model.function.FunctionFactory;
import org.fortiss.af3.exploration.dseml.model.function.Start;
import org.fortiss.af3.exploration.model.IExplorationConstraint;
import org.fortiss.af3.exploration.model.SuperSetMap;
import org.fortiss.af3.exploration.smt.AF3ExplorationSMTActivator;
import org.fortiss.af3.exploration.smt.model.SMTConstraint;
import org.fortiss.af3.platform.model.ExecutionUnit;
import org.fortiss.af3.platform.model.Route;
import org.fortiss.af3.task.model.Signal;
......@@ -70,22 +72,22 @@ public class BasicDeploymentConstraint {
* @throws Exception
* if a start/end point of a signal is not referenced in the super sets.
*/
public static List<SMTConstraint> createBasicSignalConstraints(SuperSetMap superSetMap)
throws Exception {
public static List<IExplorationConstraint<?>>
createBasicSignalConstraints(SuperSetMap superSetMap) throws Exception {
SuperSet<Signal> signalSuperSet = superSetMap.get(Signal.class);
SuperSet<Task> taskSuperSet = superSetMap.get(Task.class);
SuperSet<ExecutionUnit> ecuSuperSet = superSetMap.get(ExecutionUnit.class);
SuperSet<Route> routeSuperSet = superSetMap.get(Route.class);
List<SMTConstraint> constraints = new ArrayList<>();
List<IExplorationConstraint<?>> constraints = new ArrayList<>();
SMTConstraint routingCstrs =
IExplorationConstraint<?> routingCstrs =
createBasicRoutingConstraints(signalSuperSet, routeSuperSet, superSetMap);
if(routingCstrs != null) {
constraints.add(routingCstrs);
}
List<SMTConstraint> startEndCstrs;
List<IExplorationConstraint<?>> startEndCstrs;
try {
startEndCstrs = createStartEndConstraints(signalSuperSet, routeSuperSet, taskSuperSet,
ecuSuperSet);
......@@ -118,8 +120,9 @@ public class BasicDeploymentConstraint {
* @return Basic rooting constraint, or {@code null} in case it could not be created.
*
*/
private static SMTConstraint createBasicRoutingConstraints(SuperSet<Signal> signalSuperSet,
SuperSet<Route> routes, SuperSetMap dseSuperSets) throws Exception {
private static IExplorationConstraint<?> createBasicRoutingConstraints(
SuperSet<Signal> signalSuperSet, SuperSet<Route> routes, SuperSetMap dseSuperSets)
throws Exception {
Set<Signal> channels = createSet(signalSuperSet, signalSuperSet.getEntries(), Signal.class);
// ensure get(0) is valid
if(signalSuperSet.getEntries().isEmpty() || signalSuperSet.getEntries().get(0) == null) {
......@@ -169,7 +172,8 @@ public class BasicDeploymentConstraint {
Implies implies = createImplies(allocationCH_Route, createAnd);
forAllRoutes.setExpression(implies);
return createSMTConstraint("Basic Deployment Constraint", forAllCH, true);
return createExplorationConstraint(Boolean.class, createResourceDimension(), forAllCH,
"Basic Routing Constraint", true);
}
/** Creates an {@link Start} literal. */
......@@ -193,19 +197,20 @@ public class BasicDeploymentConstraint {
}
/** Creates a fixed start and end constraint for all allocationSources and paths. */
private static List<SMTConstraint> createStartEndConstraints(SuperSet<Signal> signalSuperSet,
SuperSet<Route> routes, SuperSet<Task> taskSuperSet, SuperSet<ExecutionUnit> ecuSet)
throws UnsupportedDataTypeException {
List<SMTConstraint> expressions = new ArrayList<>();
private static List<IExplorationConstraint<?>> createStartEndConstraints(
SuperSet<Signal> signalSuperSet, SuperSet<Route> routes, SuperSet<Task> taskSuperSet,
SuperSet<ExecutionUnit> ecuSet) throws UnsupportedDataTypeException {
List<IExplorationConstraint<?>> expressions = new ArrayList<>();
createRouteConstraints(routes, ecuSet, expressions);
createSignalConstraints(signalSuperSet, taskSuperSet, expressions);
return expressions;
}
/** Creates a single {@link Start} or {@link End} constraint. */
private static <S extends IModelElement, T extends IModelElement> SMTConstraint
createStartEndConstraint(SuperSet<S> superSet1, SuperSet<T> superSet2, S element1,
T element2, String element1Name, String element2Name,
private static <S extends IModelElement, T extends IModelElement>
IExplorationConstraint<Boolean> createStartEndConstraint(SuperSet<S> superSet1,
SuperSet<T> superSet2, S element1, T element2, String element1Name,
String element2Name,
BiFunction<Set<IModelElement>, Set<IModelElement>, Equal> cmpFnc,
String constraintName) {
......@@ -228,12 +233,13 @@ public class BasicDeploymentConstraint {
Equal equals = cmpFnc.apply(channelsModelElementSet, tasksModelElementSet);
forAllComp.setExpression(equals);
return createSMTConstraint(constraintName, forAllCH, true);
return createExplorationConstraint(Boolean.class, createTemporalDimension(), forAllCH,
constraintName, true);
}
/** Creates start and end constraints of {@link IConnection}s. */
private static void createSignalConstraints(SuperSet<Signal> signalSuperSet,
SuperSet<Task> taskSuperSet, List<SMTConstraint> expressions)
SuperSet<Task> taskSuperSet, List<IExplorationConstraint<?>> expressions)
throws UnsupportedDataTypeException {
for(Signal channel : signalSuperSet.getEntries()) {
TaskOutputPort s = channel.getSourceTaskPort();
......@@ -251,14 +257,14 @@ public class BasicDeploymentConstraint {
"Target of connection " + channel + " can not be found");
}
// start
SMTConstraint startConstraint = createStartEndConstraint(signalSuperSet, taskSuperSet,
channel, source, "Signal", "Task", BasicDeploymentConstraint::start,
"Start Channel Constraints");
IExplorationConstraint<Boolean> startConstraint = createStartEndConstraint(
signalSuperSet, taskSuperSet, channel, source, "Signal", "Task",
BasicDeploymentConstraint::start, "Start Channel Constraints");
expressions.add(startConstraint);
// end
SMTConstraint endConstraint = createStartEndConstraint(signalSuperSet, taskSuperSet,
channel, target, "Signal", "Task", BasicDeploymentConstraint::end,
IExplorationConstraint<Boolean> endConstraint = createStartEndConstraint(signalSuperSet,
taskSuperSet, channel, target, "Signal", "Task", BasicDeploymentConstraint::end,
"End Channel Constraints");
expressions.add(endConstraint);
}
......@@ -266,7 +272,7 @@ public class BasicDeploymentConstraint {
/** Creates start and end constraints for {@link Route}s. */
private static void createRouteConstraints(SuperSet<Route> routes,
SuperSet<ExecutionUnit> ecuSet, List<SMTConstraint> expressions)
SuperSet<ExecutionUnit> ecuSet, List<IExplorationConstraint<?>> expressions)
throws UnsupportedDataTypeException {
for(Route route : routes.getEntries()) {
ExecutionUnit ecuStart = route.getSenderExecutionUnit();
......@@ -281,12 +287,12 @@ public class BasicDeploymentConstraint {
"Target of route " + route + " can not be found");
}
SMTConstraint startConstraint =
IExplorationConstraint<Boolean> startConstraint =
createStartEndConstraint(routes, ecuSet, route, ecuStart, "Route", "ECU",
BasicDeploymentConstraint::start, "Start Route Constraints");
expressions.add(startConstraint);
SMTConstraint endConstraint =
IExplorationConstraint<Boolean> endConstraint =
createStartEndConstraint(routes, ecuSet, route, ecuEnd, "Route", "ECU",
BasicDeploymentConstraint::end, "End Route Constraints");
expressions.add(endConstraint);
......