Skip to content
GitLab
Commit 72e48dd1 authored by Simon Barner's avatar Simon Barner
Browse files

Merge branch '3541' into 'master' 

3541

See merge request af3/af3!363
parents cb09957f 688c122a
Hide whitespace changes
Inline Side-by-side
org.fortiss.af3.exploration.smt/META-INF/MANIFEST.MF
View file @ 72e48dd1
......@@ -14,8 +14,18 @@ Require-Bundle: org.fortiss.af3.exploration,
com.microsoft.z3,
org.fortiss.af3.platform.hierarchic,
org.fortiss.af3.safety;visibility:=reexport,
org.fortiss.tooling.kernel.ui
Export-Package: org.fortiss.af3.exploration.smt.backend,
org.fortiss.tooling.kernel.ui,
com.google.guava
Export-Package: org.fortiss.af3.exploration.smt,
org.fortiss.af3.exploration.smt.backend,
org.fortiss.af3.exploration.smt.migrate,
org.fortiss.af3.exploration.smt.model,
org.fortiss.af3.exploration.smt.model.dseml,
org.fortiss.af3.exploration.smt.model.dseml.impl,
org.fortiss.af3.exploration.smt.model.dseml.util,
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.solver,
org.fortiss.af3.exploration.smt.util,
test.org.fortiss.af3.exploration.smt
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/backend/.ratings
View file @ 72e48dd1
Z3Backend.java d58fc12855dc3597e52fe0fe59cb2607d77d5583 GREEN
Z3Backend.java 1ba4698b984ea240a0143cd49730ed929607d365 GREEN
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/backend/Z3Backend.java
View file @ 72e48dd1
......@@ -15,41 +15,32 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.backend;
import static org.fortiss.af3.exploration.smt.modeltransformation.BasicDeploScheduleConstraint.generateDeploScheduleConstraints;
import static org.fortiss.af3.exploration.smt.modeltransformation.BasicDeploScheduleConstraint.generateDeploScheduleSpecificConstraints;
import static org.fortiss.af3.exploration.smt.modeltransformation.BasicDeploymentConstraint.createBasicSignalConstraints;
import static com.google.common.collect.Sets.newHashSet;
import static org.fortiss.af3.exploration.service.IDSEBackend.EXPLORATION_TYPE.FEASIBILITY_CHECK;
import static org.fortiss.af3.exploration.service.IDSEBackend.EXPLORATION_TYPE.OPTIMIZATION;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createSolverSettings;
import static org.fortiss.af3.exploration.util.ExplorationUtils.isDebugVerboseEnabled;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
import org.eclipse.core.runtime.IProgressMonitor;
import org.fortiss.af3.exploration.model.ExplorationSpecification;
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.SolverSettings;
import org.fortiss.af3.exploration.model.solutions.ExplorationSolution;
import org.fortiss.af3.exploration.model.synthesiscategory.IDeploymentSynthesis;
import org.fortiss.af3.exploration.model.synthesiscategory.IPlatformSynthesis;
import org.fortiss.af3.exploration.model.synthesiscategory.IScheduleSynthesis;
import org.fortiss.af3.exploration.model.synthesiscategory.ISynthesisCategory;
import org.fortiss.af3.exploration.service.IDSEBackend;
import org.fortiss.af3.exploration.smt.modeltransformation.BasicScheduleConstraint;
import org.fortiss.af3.exploration.smt.modeltransformation.DeploScheduleRun;
import org.fortiss.af3.exploration.smt.modeltransformation.DeploymentRun;
import org.fortiss.af3.exploration.smt.modeltransformation.ScheduleRun;
import org.fortiss.af3.exploration.smt.modeltransformation.SolverRun;
import org.fortiss.af3.platform.model.ExecutionUnit;
import org.fortiss.af3.platform.model.Route;
import org.fortiss.af3.schedule.model.ResourceAllocation;
import org.fortiss.af3.schedule.model.Schedule;
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.af3.task.model.allocation.TaskToExecutionUnitAllocationEntry;
import org.fortiss.af3.task.model.allocation.TaskToExecutionUnitAllocationTable;
import org.fortiss.af3.task.model.allocation.TaskWcetTable;
import org.fortiss.tooling.base.model.element.IModelElement;
import org.fortiss.af3.exploration.smt.solver.DeploScheduleRun;
import org.fortiss.af3.exploration.smt.solver.DeploymentRun;
import org.fortiss.af3.exploration.smt.solver.ScheduleRun;
import org.fortiss.af3.exploration.smt.solver.SolverRun;
/**
* DSE backend that uses Z3 to solve a given DSE problem. It translates a problem statement in form
......@@ -60,6 +51,9 @@ import org.fortiss.tooling.base.model.element.IModelElement;
*/
public class Z3Backend implements IDSEBackend {
/** Default timeout value in ms. */
private static int DEFAULT_TIMEOUT = 50 * 1000;
/** {@inheritDoc} */
@Override
public void validateExplorationSpecification(ExplorationSpecification spec) throws Exception {
......@@ -68,84 +62,44 @@ public class Z3Backend implements IDSEBackend {
/** {@inheritDoc} */
@Override
public Set<Class<?>> getSynthesizedArtifacts() {
Set<Class<?>> synthArtifacts = new HashSet<>();
synthArtifacts.add(TaskToExecutionUnitAllocationTable.class);
synthArtifacts.add(Schedule.class);
return synthArtifacts;
public Map<Class<? extends ISynthesisCategory>, String> getSynthesisTypes() {
Map<Class<? extends ISynthesisCategory>, String> catMap = new HashMap<>();
catMap.put(IPlatformSynthesis.class, "Platform");
catMap.put(IDeploymentSynthesis.class, "Deployment");
catMap.put(IScheduleSynthesis.class, "Schedule");
return catMap;
}
/** {@inheritDoc} */
@Override
public Optional<ExplorationSolution> executeDSE(ExplorationSpecification spec,
Set<Class<? extends IModelElement>> solutionTypes, IProgressMonitor monitor,
int timeoutMS) throws Exception {
// For SMT, we must add constraints in the correct order: user last.
List<IExplorationTarget<?>> inputTargets = new ArrayList<>(spec.getTargets());
spec.getTargets().clear();
public Set<EXPLORATION_TYPE> getExplorationTypes() {
return newHashSet(FEASIBILITY_CHECK, OPTIMIZATION);
}
List<IExplorationTarget<?>> basicConstraints = new ArrayList<>();
/** {@inheritDoc} */
@Override
public SolverSettings getSolverSettings() {
return createSolverSettings(DEFAULT_TIMEOUT, 0);
}
SuperSetMap superSets = spec.getSearchSpace();
/** {@inheritDoc} */
@Override
public Optional<ExplorationSolution> executeDSE(ExplorationSpecification spec,
SolverSettings settings, IProgressMonitor monitor) throws Exception {
SolverRun solverRun;
if(solutionTypes.contains(TaskToExecutionUnitAllocationTable.class)) {
// Add SMT-specific constraints to define the basic deployment problem.
basicConstraints.addAll(createBasicSignalConstraints(superSets));
if(solutionTypes.contains(Schedule.class)) {
// Case deployment+schedule run
// Add SMT-specific constraints to define the deployment+schedule problem.
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));
basicConstraints.addAll(basicDeploScheduleConstraints);
// TODO (#3361): Generation of causality constraints is for now kept separated,
// because of the different treatment of routing in the pure schedule case
basicConstraints.addAll(generateDeploScheduleSpecificConstraints(superSets));
if(isDebugVerboseEnabled()) {
System.out.println("DeploScheduleRun");
}
solverRun = new DeploScheduleRun();
} else {
// Case pure deployment run
if(isDebugVerboseEnabled()) {
System.out.println("DeploymentRun");
}
solverRun = new DeploymentRun();
}
int timeout = settings.getTermination().getTimeoutMS().getValue();
Collection<Class<? extends ISynthesisCategory>> synthTypes = spec.getSynthTypes();
if(synthTypes.contains(IDeploymentSynthesis.class) &&
synthTypes.contains(IScheduleSynthesis.class)) {
solverRun = new DeploScheduleRun(spec, timeout);
} else if(synthTypes.contains(IDeploymentSynthesis.class)) {
solverRun = new DeploymentRun(spec, timeout);
} else if(synthTypes.contains(IScheduleSynthesis.class)) {
solverRun = new ScheduleRun(spec, timeout);
} else {
// Case pure schedule run
// Add SMT-specific constraints to define the deployment+schedule problem.
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<IExplorationConstraint<?>> basicScheduleConstraints = BasicScheduleConstraint
.generatePureScheduleConstraints(superSets.get(ResourceAllocation.class),
superSets.get(Task.class), superSets.get(ExecutionUnit.class),
superSets.get(ComponentToTaskAllocationEntry.class),
superSets.get(TaskToExecutionUnitAllocationEntry.class),
superSets.get(SignalToRouteAllocationEntry.class));
basicConstraints.addAll(basicDeploScheduleConstraints);
basicConstraints.addAll(basicScheduleConstraints);
if(isDebugVerboseEnabled()) {
System.out.println("ScheduleRun");
}
solverRun = new ScheduleRun();
}
spec.getTargets().addAll(basicConstraints);
spec.getTargets().addAll(inputTargets);
if(spec.getTargets().isEmpty()) {
throw new Exception("No exploration targets defined. Cannot perform DSE.");
throw new Exception("No applicable " + SolverRun.class.getSimpleName() +
" was found for the given set of syntesises to perform.");
}
if(isDebugVerboseEnabled()) {
......@@ -158,13 +112,8 @@ public class Z3Backend implements IDSEBackend {
i++;
}
}
ExplorationSolution expSolution = solverRun.solve(spec, timeoutMS, monitor);
// Remove additional input sets (that have potentially been created on the fly)
// as well as basic constraints (only user-defined constraints shall be persisted)
superSets.removeKey(ResourceAllocation.class);
superSets.removeKey(SignalToRouteAllocationEntry.class);
spec.getTargets().removeAll(basicConstraints);
ExplorationSolution expSolution = solverRun.solve(monitor);
return Optional.of(expSolution);
}
......
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/migrate/.ratings
View file @ 72e48dd1
SMTExplorationTargetMigrator.java 843c5e4b8ddb7ddb1ca6f670da6b3d3bb839fe88 GREEN
SMTExplorationTargetMigrator.java c5cf1a5f40ea0a3c1b0940bdbb57950584d44af6 GREEN
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/migrate/SMTExplorationTargetMigrator.java
View file @ 72e48dd1
......@@ -15,6 +15,7 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.migrate;
import static com.google.common.collect.Sets.newHashSet;
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;
......@@ -35,6 +36,7 @@ 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.model.synthesiscategory.IDeploymentSynthesis;
import org.fortiss.af3.exploration.smt.model.CustomDimension;
import org.fortiss.af3.exploration.smt.model.SMTConstraint;
import org.fortiss.af3.exploration.smt.model.SMTObjective;
......@@ -44,7 +46,7 @@ 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.
* unified {@link IExplorationTarget}s.
*
* @author diewald
*/
......@@ -91,7 +93,8 @@ public class SMTExplorationTargetMigrator implements IMigrationProvider {
for(SMTConstraint constraint : getChildrenWithType(dse, SMTConstraint.class)) {
ExplorationConstraint<Boolean> newConstraint = createExplorationConstraint(
Boolean.class, createUserDefinedDimension(constraint.getDimension()),
constraint.getExpression(), constraint.getName(), constraint.isImplicit());
newHashSet(IDeploymentSynthesis.class), constraint.getExpression(),
constraint.getName(), constraint.isImplicit());
replace(constraint, newConstraint);
oldNewMap.put(constraint, newConstraint);
......
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/modeltransformation/.ratings
View file @ 72e48dd1
BasicDeploScheduleConstraint.java 76029b866e82f7fcbb78292e366a41d39ad86cdc GREEN
BasicDeploymentConstraint.java bd66d1e997b091ddd28423529de5a5c23af1bee9 GREEN
BasicScheduleConstraint.java 8b054b5ad961295b97936e26240eb33a10a1ee9a GREEN
ConstraintDefinitionUtils.java b4cea0e5aabef8314c35ac22e9fabb32458e1f05 GREEN
BasicDeploScheduleConstraint.java c278ce01fdf33ac04de345040261893686237845 GREEN
BasicDeploymentConstraint.java 06515032af8bac566160d16c14fff0d44365b0d2 GREEN
BasicScheduleConstraint.java f8f5b991f1cc90ec129ef33b5575c68e49b08a7b GREEN
ConstraintTransformationAdapter.java 8806164d71491c7d1af665990dd154f2275cad8c GREEN
DSMLTransformationService.java 7869a480c0fccb5f75677b392a5d1dd1a3328b5c GREEN
DSMLtoSMTTransformator.java 0e750ee0a344b1913774d1a83a8568ff09f49436 GREEN
DefaultExpressionTransformator.java 34733e33b3a55eef0fdda724b74fe181beaa7f2d GREEN
DeploScheduleRun.java 2b07bd6b40cf4ce2eabc12198f6db3b9655bed25 GREEN
DeploymentRun.java 4b2d0a6d64bb5a6efabc2ee9bf933cc523843ac8 GREEN
EnergyConstraintDefinition.java c43979cfc30e626d597de6860a13dc42c30b677c GREEN
DSMLTransformationService.java 642825f94e172094f7412e9e3e8f7f35414c8228 GREEN
DSMLtoSMTTransformator.java 29663e8526f5c7d3acd85eab4f5609b9f0fcba54 GREEN
DefaultExpressionTransformator.java b890bc609fe9cc45c0af88524ae83cf367ccaee4 GREEN
EnergyConstraintDefinition.java f394e4195ed678ae294b48dbe3c39c783f9c927d GREEN
ExpressionTransformator.java 81dfc30221e519aa8175693353ace8992687327f GREEN
IDSMLTransformationService.java 0bbcefa52d1127250697ca3d92a1b810db1b8871 GREEN
NonQuantifiedExpressionTransformator.java 9ee437aeaf518d94b81e34a275cd01b87cfca1bf GREEN
QuantifiedExpressionTransformator.java 01e7162b24d16adb23f646cf02340879e8a18205 GREEN
SMTTransformationUtils.java 14f70ea23c0589b5105dae9f7034a99eb3f72606 GREEN
ScheduleRun.java 43d869a9adfbebe34c34f1ebb0bc8e0600f45b9d GREEN
SolverRun.java ff3c69cf4fed2007f7f6bbeaefb4a2343d3c2e8d GREEN
TimingConstraintDefinition.java 92281277d99bb52b72c1cb898bba944b3b9a24f7 GREEN
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/modeltransformation/BasicDeploScheduleConstraint.java
View file @ 72e48dd1
......@@ -15,32 +15,27 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.modeltransformation;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.createDurationLiteral;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.createEnd;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.createFrequencyAssigned;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.createScheduledSignal;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.createScheduledTask;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.createStart;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.createStartTimeLiteral;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.defineAllocation;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.defineIsTask;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.defineStronglyCausal;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.generateForAll;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.getAdmissibleFrequencies;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.getMinBandwidth;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.getSignal;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.isLocal;
import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefinitionUtils.isStronglyCausal;
import static com.google.common.collect.Sets.newHashSet;
import static org.fortiss.af3.exploration.smt.modeltransformation.EnergyConstraintDefinition.createFrequencyConstraints;
import static org.fortiss.af3.exploration.smt.modeltransformation.EnergyConstraintDefinition.createMinimizeConsumptionObjective;
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.util.DSEProjectModelElementFactory.createRuleSet;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.createEnd;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.createFrequencyAssigned;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.createScheduledSignal;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.createScheduledTask;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.createStart;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.defineAllocation;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.defineIsTask;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.defineStronglyCausal;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.getAdmissibleFrequencies;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.getMinBandwidth;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.getSignal;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.isLocal;
import static org.fortiss.af3.exploration.smt.util.ConstraintDefinitionUtils.isStronglyCausal;
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.createArithmeticLiteral;
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.createGreaterEqual;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createImplies;
import static org.fortiss.af3.exploration.util.DSMLModelElementFactory.createLessEqual;
......@@ -49,22 +44,19 @@ 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.exploration.util.ExplorationTimingConstraintUtils.createDurationLiteral;
import static org.fortiss.af3.exploration.util.ExplorationTimingConstraintUtils.createStartTimeLiteral;
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;
import static org.fortiss.tooling.kernel.utils.KernelModelElementUtils.runAsCommand;
import static org.fortiss.tooling.kernel.utils.UniqueIDUtils.prepareUniqueID;
import java.math.BigDecimal;
import java.util.ArrayList;
import java.util.Date;
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.ArithmeticPropertyLiteral;
......@@ -82,17 +74,14 @@ import org.fortiss.af3.exploration.dseml.model.booleanp.comparison.NotEqual;
import org.fortiss.af3.exploration.dseml.model.expression.ModelElementLiteral;
import org.fortiss.af3.exploration.dseml.model.expression.Set;
import org.fortiss.af3.exploration.dseml.model.expression.SuperSet;
import org.fortiss.af3.exploration.dseml.model.function.IFunction;
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.model.synthesiscategory.IDeploymentSynthesis;
import org.fortiss.af3.exploration.model.synthesiscategory.IScheduleSynthesis;
import org.fortiss.af3.exploration.smt.model.dseml.FrequencyAssigned;
import org.fortiss.af3.platform.model.ExecutionUnit;
import org.fortiss.af3.platform.model.Route;
......@@ -105,7 +94,6 @@ import org.fortiss.af3.task.model.Task;
import org.fortiss.af3.task.model.TaskOutputPort;
import org.fortiss.af3.task.model.allocation.ComponentToTaskAllocationEntry;
import org.fortiss.af3.task.model.allocation.TaskWcetTable;
import org.fortiss.af3.timing.model.TimingSpecification;
import org.fortiss.tooling.base.model.element.IModelElement;
/**
......@@ -138,9 +126,10 @@ public class BasicDeploScheduleConstraint {
assertions.addAll(createTileFrequencyConstraints(ecuSS));
int i = 1;
for(IBooleanExpression expr : assertions) {
IExplorationConstraint<?> ts =
@SuppressWarnings("unchecked") IExplorationConstraint<?> ts =
createExplorationConstraint(Boolean.class, createUserDefinedDimension("unused"),
expr, "Implicit Schedule Constraint " + i++, true);
newHashSet(IDeploymentSynthesis.class), expr,
"Implicit Schedule Constraint " + i++, true);
generatedConstraints.add(ts);
prepareUniqueID(ts, co2ta);
}
......@@ -166,8 +155,10 @@ public class BasicDeploScheduleConstraint {
assertions.addAll(createRoutesNonOverlappingConstraints(resAllocSS));
int i = 1;
for(IBooleanExpression expr : assertions) {
IExplorationConstraint<?> ts = createExplorationConstraint(Double.class,
createTemporalDimension(), expr, "Non-Overlapping Constraint " + i++, true);
@SuppressWarnings("unchecked") IExplorationConstraint<?> ts =
createExplorationConstraint(Double.class, createTemporalDimension(),
newHashSet(IScheduleSynthesis.class), expr,
"Non-Overlapping Constraint " + i++, true);
generatedConstraints.add(ts);
prepareUniqueID(ts, superSets.get(ComponentToTaskAllocationEntry.class));
}
......@@ -176,8 +167,10 @@ public class BasicDeploScheduleConstraint {
assertions.addAll(createCausalityConstraints(resAllocSS, taskSS, signalSS, ecuSS));
i = 1;
for(IBooleanExpression expr : assertions) {
IExplorationConstraint<?> ts = createExplorationConstraint(Double.class,
createTemporalDimension(), expr, "Causality Constraint " + i++, true);
@SuppressWarnings("unchecked") IExplorationConstraint<?> ts =
createExplorationConstraint(Double.class, createTemporalDimension(),
newHashSet(IScheduleSynthesis.class), expr,
"Causality Constraint " + i++, true);
generatedConstraints.add(ts);
prepareUniqueID(ts, superSets.get(ComponentToTaskAllocationEntry.class));
}
......@@ -201,7 +194,7 @@ public class BasicDeploScheduleConstraint {
createStartTimeLiteral(set);
ArithmeticLiteral literal = createArithmeticLiteral(BigDecimal.ZERO);
GreaterEqual gEquals = createGreaterEqual(startSet1, literal);
ForAll forAll1 = generateForAll(set, gEquals, true);
ForAll forAll1 = createForAll(set, gEquals, true);
assertions.add(forAll1);
return assertions;
......@@ -228,7 +221,7 @@ public class BasicDeploScheduleConstraint {
Equal equality = defineStronglyCausal(taskSet, isStronglyCausal(task, co2ta));
// quantify over the single task
ForAll formula = generateForAll(taskSet, equality, true);
ForAll formula = createForAll(taskSet, equality, true);
assertions.add(formula);
}
......@@ -258,7 +251,7 @@ public class BasicDeploScheduleConstraint {
Equal equality = defineIsTask(raSet, entity instanceof Task);
// quantify over the single task
ForAll formula = generateForAll(raSet, equality, true);
ForAll formula = createForAll(raSet, equality, true);
assertions.add(formula);
}
......@@ -293,9 +286,9 @@ public class BasicDeploScheduleConstraint {
Equal equality = createEquals(elem, ent);
// quantify over scheduled elements
ForAll forAll = generateForAll(entitySet, equality, true);
ForAll forAll = createForAll(entitySet, equality, true);
// quantify over resource allocations
ForAll formula = generateForAll(raSet, forAll, true);
ForAll formula = createForAll(raSet, forAll, true);
assertions.add(formula);
} else if(modelElement instanceof TaskOutputPort) {
......@@ -306,9 +299,9 @@ public class BasicDeploScheduleConstraint {
Equal equality = createEquals(elem, ent);
// quantify over scheduled elements
ForAll forAll = generateForAll(signalSet, equality, true);
ForAll forAll = createForAll(signalSet, equality, true);
// quantify over resource allocations
ForAll formula = generateForAll(raSet, forAll, true);
ForAll formula = createForAll(raSet, forAll, true);
assertions.add(formula);
}
......@@ -415,15 +408,15 @@ public class BasicDeploScheduleConstraint {
// forall ecu in ECUs.
// quantify over the ECUs
ForAll forAllRes = generateForAll(ecuSet1, implication, false);
ForAll forAllRes = createForAll(ecuSet1, implication, false);
// quantify over the tasks
ForAll forAllEntity1 = generateForAll(taskSet2, forAllRes, false);
ForAll forAllEntity2 = generateForAll(taskSet1, forAllEntity1, false);
ForAll forAllEntity1 = createForAll(taskSet2, forAllRes, false);
ForAll forAllEntity2 = createForAll(taskSet1, forAllEntity1, false);
// quantify over the resource allocations
ForAll forAllRA2 = generateForAll(raSet2, forAllEntity2, false);
ForAll formula = generateForAll(raSet1, forAllRA2, false);
ForAll forAllRA2 = createForAll(raSet2, forAllEntity2, false);
ForAll formula = createForAll(raSet1, forAllRA2, false);
assertions.add(formula);
return assertions;
......@@ -492,8 +485,8 @@ public class BasicDeploScheduleConstraint {
Implies implication = createImplies(premise, conclusion);
// quantify over routes, signals and resource allocations
ForAll forAllRA2 = generateForAll(raSet2, implication, false);
ForAll formula = generateForAll(raSet1, forAllRA2, false);
ForAll forAllRA2 = createForAll(raSet2, implication, false);
ForAll formula = createForAll(raSet1, forAllRA2, false);
assertions.add(formula);
return assertions;
......@@ -534,7 +527,7 @@ public class BasicDeploScheduleConstraint {
createDurationLiteral(oneElementSet);
ArithmeticLiteral literal = createArithmeticLiteral(currentRA.getDuration());
Equal equals = createEquals(literal, duration);
ForAll formula = generateForAll(oneElementSet, equals, true);
ForAll formula = createForAll(oneElementSet, equals, true);
assertions.add(formula);
}
}
......@@ -604,9 +597,9 @@ public class BasicDeploScheduleConstraint {
Implies implication = createImplies(allocation, duration);
// adds quantifiers
ForAll forAll0 = generateForAll(signalSet, implication, true);
ForAll forAll1 = generateForAll(routeSet, forAll0, true);
ForAll formula = generateForAll(ra, forAll1, true);
ForAll forAll0 = createForAll(signalSet, implication, true);
ForAll forAll1 = createForAll(routeSet, forAll0, true);
ForAll formula = createForAll(ra, forAll1, true);
assertions.add(formula);
}
......@@ -658,16 +651,15 @@ public class BasicDeploScheduleConstraint {
ArithmeticPropertyLiteral<ResourceAllocation, Number> duration =
createDurationLiteral(ra);
BigDecimal value = getWcet(taskWcetTable, (Task)modelElement, ecu, frequency);
int valueInt = value.intValue();
ArithmeticLiteral valueLiteral = createArithmeticLiteral(new BigDecimal(valueInt));
ArithmeticLiteral valueLiteral = createArithmeticLiteral(value);
Equal conclusion = createEquals(duration, valueLiteral);
// create implication
Implies implication = createImplies(premise, conclusion);
ForAll forall = generateForAll(ra, implication, true);
ForAll forall2 = generateForAll(ecuSet, forall, true);
ForAll formula = generateForAll(taskSet, forall2, tr