Commit ef7a0869 authored by Alexander Diewald's avatar Alexander Diewald

Merge branch '3365' into 4008

Conflicts:
	org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/modeltransformation/.ratings
	org.fortiss.af3.exploration/src/org/fortiss/af3/exploration/util/.ratings
Signed-off-by: Alexander Diewald's avatarAlexander Diewald <diewald@fortiss.org>
parents 771b183f 8365bf66
...@@ -16,9 +16,6 @@ Require-Bundle: org.fortiss.af3.exploration, ...@@ -16,9 +16,6 @@ Require-Bundle: org.fortiss.af3.exploration,
org.fortiss.af3.safety;visibility:=reexport, org.fortiss.af3.safety;visibility:=reexport,
org.fortiss.tooling.kernel.ui org.fortiss.tooling.kernel.ui
Export-Package: org.fortiss.af3.exploration.smt.backend, 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.modeltransformation,
org.fortiss.af3.exploration.smt.util, org.fortiss.af3.exploration.smt.util,
test.org.fortiss.af3.exploration.smt test.org.fortiss.af3.exploration.smt
model.ecore 3159422b58b66acc4c36ccc8e318a2b9b1773da5 GREEN model.ecore 3e1b36f950369b789a95159d87158218d3628a41 YELLOW
...@@ -3,7 +3,7 @@ ...@@ -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"> 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"> <eClassifiers xsi:type="ecore:EClass" name="SMTConstraint">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel"> <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> </eAnnotations>
<eGenericSuperTypes eClassifier="ecore:EClass platform:/resource/org.fortiss.af3.exploration/model/exploration.ecore#//ExplorationConstraint"> <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"/> <eTypeArguments eClassifier="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBooleanObject"/>
...@@ -12,7 +12,7 @@ ...@@ -12,7 +12,7 @@
</eClassifiers> </eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="SMTObjective"> <eClassifiers xsi:type="ecore:EClass" name="SMTObjective">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel"> <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> </eAnnotations>
<eStructuralFeatures xsi:type="ecore:EReference" name="constraints" upperBound="-1" <eStructuralFeatures xsi:type="ecore:EReference" name="constraints" upperBound="-1"
eType="#//SMTConstraint" containment="true"> eType="#//SMTConstraint" containment="true">
...@@ -25,9 +25,9 @@ ...@@ -25,9 +25,9 @@
</eGenericSuperTypes> </eGenericSuperTypes>
<eGenericSuperTypes eClassifier="#//CustomDimension"/> <eGenericSuperTypes eClassifier="#//CustomDimension"/>
</eClassifiers> </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"> <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> </eAnnotations>
<eStructuralFeatures xsi:type="ecore:EAttribute" name="dimension" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString" <eStructuralFeatures xsi:type="ecore:EAttribute" name="dimension" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"
defaultValueLiteral="category"> defaultValueLiteral="category">
......
...@@ -11,4 +11,13 @@ ...@@ -11,4 +11,13 @@
class="org.fortiss.af3.exploration.smt.model.AF3ExplorationSMTPackage" class="org.fortiss.af3.exploration.smt.model.AF3ExplorationSMTPackage"
genModel="model/model.genmodel"/> genModel="model/model.genmodel"/>
</extension> </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> </plugin>
Z3Backend.java f9cb53217d533e7014cc32fceee9d6922d145f4e GREEN Z3Backend.java 070f627218b36e50f61c56d850d0679e5a69d332 YELLOW
...@@ -28,12 +28,12 @@ import java.util.Set; ...@@ -28,12 +28,12 @@ import java.util.Set;
import org.eclipse.core.runtime.IProgressMonitor; import org.eclipse.core.runtime.IProgressMonitor;
import org.fortiss.af3.exploration.model.ExplorationSpecification; 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.SuperSetMap;
import org.fortiss.af3.exploration.model.solutions.ExplorationSolution; import org.fortiss.af3.exploration.model.solutions.ExplorationSolution;
import org.fortiss.af3.exploration.service.DSESolutionVisualization; import org.fortiss.af3.exploration.service.DSESolutionVisualization;
import org.fortiss.af3.exploration.service.IDSEBackend; 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.BasicScheduleConstraint;
import org.fortiss.af3.exploration.smt.modeltransformation.DeploScheduleRun; import org.fortiss.af3.exploration.smt.modeltransformation.DeploScheduleRun;
import org.fortiss.af3.exploration.smt.modeltransformation.DeploymentRun; import org.fortiss.af3.exploration.smt.modeltransformation.DeploymentRun;
...@@ -84,10 +84,10 @@ public class Z3Backend implements IDSEBackend { ...@@ -84,10 +84,10 @@ public class Z3Backend implements IDSEBackend {
Set<Class<? extends IModelElement>> solutionTypes, IProgressMonitor monitor, Set<Class<? extends IModelElement>> solutionTypes, IProgressMonitor monitor,
int timeoutMS) throws Exception { int timeoutMS) throws Exception {
// For SMT, we must add constraints in the correct order: user last. // 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(); spec.getTargets().clear();
List<ExplorationTarget<?>> basicConstraints = new ArrayList<>(); List<IExplorationTarget<?>> basicConstraints = new ArrayList<>();
SuperSetMap superSets = spec.getSearchSpace(); SuperSetMap superSets = spec.getSearchSpace();
SolverRun solverRun; SolverRun solverRun;
...@@ -99,7 +99,7 @@ public class Z3Backend implements IDSEBackend { ...@@ -99,7 +99,7 @@ public class Z3Backend implements IDSEBackend {
if(solutionTypes.contains(Schedule.class)) { if(solutionTypes.contains(Schedule.class)) {
// Case deployment+schedule run // Case deployment+schedule run
// Add SMT-specific constraints to define the deployment+schedule problem. // Add SMT-specific constraints to define the deployment+schedule problem.
List<SMTConstraint> basicDeploScheduleConstraints = List<IExplorationConstraint<?>> basicDeploScheduleConstraints =
generateDeploScheduleConstraints(superSets.get(ResourceAllocation.class), generateDeploScheduleConstraints(superSets.get(ResourceAllocation.class),
superSets.get(Task.class), superSets.get(Signal.class), superSets.get(Task.class), superSets.get(Signal.class),
superSets.get(ExecutionUnit.class), superSets.get(Route.class), superSets.get(ExecutionUnit.class), superSets.get(Route.class),
...@@ -123,14 +123,15 @@ public class Z3Backend implements IDSEBackend { ...@@ -123,14 +123,15 @@ public class Z3Backend implements IDSEBackend {
} else { } else {
// Case pure schedule run // Case pure schedule run
// Add SMT-specific constraints to define the deployment+schedule problem. // Add SMT-specific constraints to define the deployment+schedule problem.
List<SMTConstraint> basicDeploScheduleConstraints = generateDeploScheduleConstraints( List<IExplorationConstraint<?>> basicDeploScheduleConstraints =
superSets.get(ResourceAllocation.class), superSets.get(Task.class), generateDeploScheduleConstraints(superSets.get(ResourceAllocation.class),
superSets.get(Signal.class), superSets.get(ExecutionUnit.class), superSets.get(Task.class), superSets.get(Signal.class),
superSets.get(Route.class), superSets.get(ComponentToTaskAllocationEntry.class), superSets.get(ExecutionUnit.class), superSets.get(Route.class),
superSets.get(TaskWcetTable.class)); superSets.get(ComponentToTaskAllocationEntry.class),
superSets.get(TaskWcetTable.class));
// Add SMT-specific constraints to define the schedule problem, in the case when a // Add SMT-specific constraints to define the schedule problem, in the case when a
// deployment is given // deployment is given
List<SMTConstraint> basicScheduleConstraints = BasicScheduleConstraint List<IExplorationConstraint<?>> basicScheduleConstraints = BasicScheduleConstraint
.generatePureScheduleConstraints(superSets.get(ResourceAllocation.class), .generatePureScheduleConstraints(superSets.get(ResourceAllocation.class),
superSets.get(Task.class), superSets.get(ExecutionUnit.class), superSets.get(Task.class), superSets.get(ExecutionUnit.class),
superSets.get(ComponentToTaskAllocationEntry.class), superSets.get(ComponentToTaskAllocationEntry.class),
...@@ -154,7 +155,7 @@ public class Z3Backend implements IDSEBackend { ...@@ -154,7 +155,7 @@ public class Z3Backend implements IDSEBackend {
// prints on screen the list of constraints for this run // prints on screen the list of constraints for this run
int i = 1; int i = 1;
System.out.println("*** List of constraints ***"); 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(" ExplorationTarget " + i + " : " + et);
System.out.println(et.getExpression()); System.out.println(et.getExpression());
i++; i++;
......
SMTExplorationTargetMigrator.java 843c5e4b8ddb7ddb1ca6f670da6b3d3bb839fe88 YELLOW
/*-------------------------------------------------------------------------+
| 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 BasicDeploScheduleConstraint.java 76029b866e82f7fcbb78292e366a41d39ad86cdc YELLOW
BasicDeploymentConstraint.java f66c59adfa5a1619db1f1178c95fe7a4b7930d6e GREEN BasicDeploymentConstraint.java bd66d1e997b091ddd28423529de5a5c23af1bee9 YELLOW
BasicScheduleConstraint.java 87edb7bb45fa9b347f34b32c816e23189a697576 GREEN BasicScheduleConstraint.java 8b054b5ad961295b97936e26240eb33a10a1ee9a YELLOW
ConstraintDefinitionUtils.java 8a709a9cd10edd36d1ac3ed0ded0c938aa010f12 GREEN ConstraintDefinitionUtils.java 8a709a9cd10edd36d1ac3ed0ded0c938aa010f12 GREEN
ConstraintTransformationAdapter.java 8806164d71491c7d1af665990dd154f2275cad8c GREEN ConstraintTransformationAdapter.java 8806164d71491c7d1af665990dd154f2275cad8c GREEN
DSMLTransformationService.java 2c19395bffa10cdaf2e7f38fdb592254289e659c GREEN DSMLTransformationService.java 2c19395bffa10cdaf2e7f38fdb592254289e659c GREEN
DSMLtoSMTTransformator.java c4f76eef0fece9eb87f4588f37ded3183f66ef4b GREEN DSMLtoSMTTransformator.java 32431ae9bcbca84d1c7cb9726f77af67019da250 YELLOW
DefaultExpressionTransformator.java 9f572be21d1d96bc3d7604695678e57035a1b82e GREEN DefaultExpressionTransformator.java 9f572be21d1d96bc3d7604695678e57035a1b82e GREEN
DeploScheduleRun.java 2b07bd6b40cf4ce2eabc12198f6db3b9655bed25 GREEN DeploScheduleRun.java 2b07bd6b40cf4ce2eabc12198f6db3b9655bed25 GREEN
DeploymentRun.java 4b2d0a6d64bb5a6efabc2ee9bf933cc523843ac8 GREEN DeploymentRun.java 4b2d0a6d64bb5a6efabc2ee9bf933cc523843ac8 GREEN
...@@ -15,5 +15,5 @@ NonQuantifiedExpressionTransformator.java 9ee437aeaf518d94b81e34a275cd01b87cfca1 ...@@ -15,5 +15,5 @@ NonQuantifiedExpressionTransformator.java 9ee437aeaf518d94b81e34a275cd01b87cfca1
QuantifiedExpressionTransformator.java 01e7162b24d16adb23f646cf02340879e8a18205 GREEN QuantifiedExpressionTransformator.java 01e7162b24d16adb23f646cf02340879e8a18205 GREEN
SMTTransformationUtils.java 376da0f5dafb350b49004c7d75fb8858b53d3b7d GREEN SMTTransformationUtils.java 376da0f5dafb350b49004c7d75fb8858b53d3b7d GREEN
ScheduleRun.java 43d869a9adfbebe34c34f1ebb0bc8e0600f45b9d GREEN ScheduleRun.java 43d869a9adfbebe34c34f1ebb0bc8e0600f45b9d GREEN
SolverRun.java 42ad87824d5f326974156b6e0ce360da8315ab9a GREEN SolverRun.java 7b60b4cc2095baaba914e6d5278c19273602ce6c YELLOW
TimingConstraintDefinition.java c6cdc7b0d27c401cadbfa73c304cf43e56f26be7 GREEN TimingConstraintDefinition.java 92281277d99bb52b72c1cb898bba944b3b9a24f7 YELLOW
...@@ -36,8 +36,6 @@ import static org.fortiss.af3.exploration.smt.modeltransformation.EnergyConstrai ...@@ -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.createMinimizeSumObjective;
import static org.fortiss.af3.exploration.smt.modeltransformation.EnergyConstraintDefinition.createTileFrequencyConstraints; 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.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.DSEProjectModelElementFactory.createRuleSet;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createAllocation; 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.createAnd;
...@@ -51,6 +49,11 @@ import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createNot ...@@ -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.createOr;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createPlus; 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.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.af3.task.model.allocation.impl.TaskWcetTableStaticImpl.getWcet;
import static org.fortiss.tooling.base.utils.AnnotationUtils.getAnnotationValue; import static org.fortiss.tooling.base.utils.AnnotationUtils.getAnnotationValue;
import static org.fortiss.tooling.common.util.LambdaUtils.getFirst; import static org.fortiss.tooling.common.util.LambdaUtils.getFirst;
...@@ -84,12 +87,12 @@ import org.fortiss.af3.exploration.dseml.model.function.IsTask; ...@@ -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.ScheduledSignal;
import org.fortiss.af3.exploration.dseml.model.function.ScheduledTask; import org.fortiss.af3.exploration.dseml.model.function.ScheduledTask;
import org.fortiss.af3.exploration.dseml.model.function.StronglyCausal; 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.SuperSetMap;
import org.fortiss.af3.exploration.model.project.DSE; import org.fortiss.af3.exploration.model.project.DSE;
import org.fortiss.af3.exploration.model.project.ModelSnapshot; import org.fortiss.af3.exploration.model.project.ModelSnapshot;
import org.fortiss.af3.exploration.model.project.RuleSet; 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.exploration.smt.model.dseml.FrequencyAssigned;
import org.fortiss.af3.platform.model.ExecutionUnit; import org.fortiss.af3.platform.model.ExecutionUnit;
import org.fortiss.af3.platform.model.Route; import org.fortiss.af3.platform.model.Route;
...@@ -118,11 +121,11 @@ public class BasicDeploScheduleConstraint { ...@@ -118,11 +121,11 @@ public class BasicDeploScheduleConstraint {
final static int BITS_IN_A_MEGABIT = 1000000; final static int BITS_IN_A_MEGABIT = 1000000;
/** Generates standard schedule constraints for a deployment+scheduling run. */ /** 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<ResourceAllocation> resAllocSS, SuperSet<Task> taskSS,
SuperSet<Signal> signalSS, SuperSet<ExecutionUnit> ecuSS, SuperSet<Route> routeSuperSet, SuperSet<Signal> signalSS, SuperSet<ExecutionUnit> ecuSS, SuperSet<Route> routeSuperSet,
SuperSet<ComponentToTaskAllocationEntry> co2ta, SuperSet<TaskWcetTable> wcetTable) { SuperSet<ComponentToTaskAllocationEntry> co2ta, SuperSet<TaskWcetTable> wcetTable) {
List<SMTConstraint> generatedConstraints = new ArrayList<>(); List<IExplorationConstraint<?>> generatedConstraints = new ArrayList<>();
List<IBooleanExpression> assertions = new ArrayList<>(); List<IBooleanExpression> assertions = new ArrayList<>();
assertions = new ArrayList<>(); assertions = new ArrayList<>();
assertions.addAll(createStronglyCausalFunction(taskSS, co2ta)); assertions.addAll(createStronglyCausalFunction(taskSS, co2ta));
...@@ -134,8 +137,10 @@ public class BasicDeploScheduleConstraint { ...@@ -134,8 +137,10 @@ public class BasicDeploScheduleConstraint {
assertions.addAll(createFrequencyConstraints(ecuSS)); assertions.addAll(createFrequencyConstraints(ecuSS));
assertions.addAll(createTileFrequencyConstraints(ecuSS)); assertions.addAll(createTileFrequencyConstraints(ecuSS));
int i = 1; int i = 1;
for(IBooleanExpression a : assertions) { for(IBooleanExpression expr : assertions) {
SMTConstraint ts = createSMTConstraint("Implicit Schedule Constraint " + i++, a, true); IExplorationConstraint<?> ts =
createExplorationConstraint(Boolean.class, createUserDefinedDimension("unused"),
expr, "Implicit Schedule Constraint " + i++, true);
generatedConstraints.add(ts); generatedConstraints.add(ts);
prepareUniqueID(ts, co2ta); prepareUniqueID(ts, co2ta);
} }
...@@ -149,9 +154,9 @@ public class BasicDeploScheduleConstraint { ...@@ -149,9 +154,9 @@ public class BasicDeploScheduleConstraint {
* deployment+scheduling. Once that gets fixed, this method should be removed. * deployment+scheduling. Once that gets fixed, this method should be removed.
* Generates causality constraints for a deployment+scheduling run. * Generates causality constraints for a deployment+scheduling run.
*/ */
public static List<SMTConstraint> public static List<IExplorationConstraint<?>>
generateDeploScheduleSpecificConstraints(SuperSetMap superSets) { generateDeploScheduleSpecificConstraints(SuperSetMap superSets) {
List<SMTConstraint> generatedConstraints = new ArrayList<>(); List<IExplorationConstraint<?>> generatedConstraints = new ArrayList<>();
List<IBooleanExpression> assertions = new ArrayList<>(); List<IBooleanExpression> assertions = new ArrayList<>();
SuperSet<ResourceAllocation> resAllocSS = superSets.get(ResourceAllocation.class); SuperSet<ResourceAllocation> resAllocSS = superSets.get(ResourceAllocation.class);
SuperSet<Task> taskSS = superSets.get(Task.class); SuperSet<Task> taskSS = superSets.get(Task.class);
...@@ -160,8 +165,9 @@ public class BasicDeploScheduleConstraint { ...@@ -160,8 +165,9 @@ public class BasicDeploScheduleConstraint {
assertions.addAll(createECUNonOverlappingConstraints(resAllocSS, taskSS, ecuSS)); assertions.addAll(createECUNonOverlappingConstraints(resAllocSS, taskSS, ecuSS));
assertions.addAll(createRoutesNonOverlappingConstraints(resAllocSS)); assertions.addAll(createRoutesNonOverlappingConstraints(resAllocSS));
int i = 1; int i = 1;
for(IBooleanExpression a : assertions) { for(IBooleanExpression expr : assertions) {
SMTConstraint ts = createSMTConstraint("Non-Overlapping Constraint " + i++, a, true); IExplorationConstraint<?> ts = createExplorationConstraint(Double.class,
createTemporalDimension(), expr, "Non-Overlapping Constraint " + i++, true);
generatedConstraints.add(ts); generatedConstraints.add(ts);
prepareUniqueID(ts, superSets.get(ComponentToTaskAllocationEntry.class)); prepareUniqueID(ts, superSets.get(ComponentToTaskAllocationEntry.class));
} }
...@@ -169,8 +175,9 @@ public class BasicDeploScheduleConstraint { ...@@ -169,8 +175,9 @@ public class BasicDeploScheduleConstraint {
assertions.clear(); assertions.clear();
assertions.addAll(createCausalityConstraints(resAllocSS, taskSS, signalSS, ecuSS)); assertions.addAll(createCausalityConstraints(resAllocSS, taskSS, signalSS, ecuSS));
i = 1; i = 1;
for(IBooleanExpression a : assertions) { for(IBooleanExpression expr : assertions) {
SMTConstraint ts = createSMTConstraint("Causality Constraint " + i++, a, true); IExplorationConstraint<?> ts = createExplorationConstraint(Double.class,
createTemporalDimension(), expr, "Causality Constraint " + i++, true);
generatedConstraints.add(ts); generatedConstraints.add(ts);
prepareUniqueID(ts, superSets.get(ComponentToTaskAllocationEntry.class)); prepareUniqueID(ts, superSets.get(ComponentToTaskAllocationEntry.class));
} }
...@@ -836,7 +843,8 @@ public class BasicDeploScheduleConstraint { ...@@ -836,7 +843,8 @@ public class BasicDeploScheduleConstraint {
}); });
int i = 0; int i = 0;
for(IFunction o : objectives) { 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); rs.getExplorationTargets().add(oSmt);
prepareUniqueID(oSmt, dse); prepareUniqueID(oSmt, dse);
} }
...@@ -858,7 +866,8 @@ public class BasicDeploScheduleConstraint { ...@@ -858,7 +866,8 @@ public class BasicDeploScheduleConstraint {
}); });
int i = 0; int i = 0;
for(IFunction o : objectives) { 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); rs.getExplorationTargets().add(oSmt);
prepareUniqueID(oSmt, dse); prepareUniqueID(oSmt, dse);
} }
......
...@@ -15,7 +15,6 @@ ...@@ -15,7 +15,6 @@
+--------------------------------------------------------------------------*/ +--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.modeltransformation; 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.createAllocation;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createAnd; import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createAnd;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createEquals; import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createEquals;
...@@ -23,6 +22,9 @@ import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createFor ...@@ -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.createImplies;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createModelElementLiteral; 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.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 static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
import java.util.ArrayList; import java.util.ArrayList;
...@@ -43,9 +45,9 @@ import org.fortiss.af3.exploration.dseml.model.expression.SuperSet; ...@@ -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.End;
import org.fortiss.af3.exploration.dseml.model.function.FunctionFactory; import org.fortiss.af3.exploration.dseml.model.function.FunctionFactory;
import org.fortiss.af3.exploration.dseml.model.function.Start; 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.model.SuperSetMap;
import org.fortiss.af3.exploration.smt.AF3ExplorationSMTActivator; 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.ExecutionUnit;
import org.fortiss.af3.platform.model.Route; import org.fortiss.af3.platform.model.Route;
import org.fortiss.af3.task.model.Signal; import org.fortiss.af3.task.model.Signal;
...@@ -70,22 +72,22 @@ public class BasicDeploymentConstraint { ...@@ -70,22 +72,22 @@ public class BasicDeploymentConstraint {
* @throws Exception * @throws Exception
* if a start/end point of a signal is not referenced in the super sets. * if a start/end point of a signal is not referenced in the super sets.
*/ */
public static List<SMTConstraint> createBasicSignalConstraints(SuperSetMap superSetMap) public static List<IExplorationConstraint<?>>
throws Exception { createBasicSignalConstraints(SuperSetMap superSetMap) throws Exception {