Commit 10dd6868 authored by Alexander Diewald's avatar Alexander Diewald
Browse files

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



Conflicts:
	org.fortiss.af3.exploration/src/org/fortiss/af3/exploration/testgenerator/util/.ratings
	org.fortiss.af3.exploration/src/org/fortiss/af3/exploration/testgenerator/util/DseUtils.java
Signed-off-by: Alexander Diewald's avatarAlexander Diewald <diewald@fortiss.org>
parents cbd75640 db8810ae
AF3z3Activator.java 3b41854f824afc76c3f804e627ca24dc438df758 GREEN
Z3Type.java 73e319ae206d2fd456ec9430c01b5ff7fc7282d0 GREEN
Z3javaAPIWrapper.java d21fa89f50dd9afe49eaad0901384bdf99df548f GREEN
Z3javaAPIWrapper.java 563486b7205451cdb994e8aed70667f04b37239b GREEN
......@@ -234,6 +234,14 @@ public class Z3javaAPIWrapper {
/** Returns an {@link ArithExpr}: <i>expr1 / expr2</i>. */
public static ArithExpr createDivision(Context context, ArithExpr expr1, ArithExpr expr2)
throws Z3Exception {
// By default, the context.mkDiv function casts real values to integer ones in a situation
// of mixed types. Here we enforce the behavior known from all major programming languages,
// where a division with a real term is executed as a floating point division.
if(expr1 instanceof RealExpr && expr2 instanceof IntExpr) {
expr2 = context.mkInt2Real((IntExpr)expr2);
} else if(expr1 instanceof IntExpr && expr2 instanceof RealExpr) {
expr1 = context.mkInt2Real((IntExpr)expr1);
}
return context.mkDiv(expr1, expr2);
}
......
......@@ -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
Z3Backend.java d58fc12855dc3597e52fe0fe59cb2607d77d5583 GREEN
Z3Backend.java 1ba4698b984ea240a0143cd49730ed929607d365 GREEN
......@@ -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);
}
......
SMTExplorationTargetMigrator.java 843c5e4b8ddb7ddb1ca6f670da6b3d3bb839fe88 GREEN
SMTExplorationTargetMigrator.java c5cf1a5f40ea0a3c1b0940bdbb57950584d44af6 GREEN
......@@ -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);
......
BasicDeploScheduleConstraint.java 76029b866e82f7fcbb78292e366a41d39ad86cdc GREEN
BasicDeploymentConstraint.java bd66d1e997b091ddd28423529de5a5c23af1bee9 GREEN
BasicScheduleConstraint.java 8b054b5ad961295b97936e26240eb33a10a1ee9a GREEN
ConstraintDefinitionUtils.java 8a709a9cd10edd36d1ac3ed0ded0c938aa010f12 GREEN
BasicDeploScheduleConstraint.java c278ce01fdf33ac04de345040261893686237845 GREEN
BasicDeploymentConstraint.java 06515032af8bac566160d16c14fff0d44365b0d2 GREEN
BasicScheduleConstraint.java f8f5b991f1cc90ec129ef33b5575c68e49b08a7b GREEN
ConstraintTransformationAdapter.java 8806164d71491c7d1af665990dd154f2275cad8c GREEN
DSMLTransformationService.java 2c19395bffa10cdaf2e7f38fdb592254289e659c GREEN
DSMLtoSMTTransformator.java 32431ae9bcbca84d1c7cb9726f77af67019da250 GREEN
DefaultExpressionTransformator.java 9f572be21d1d96bc3d7604695678e57035a1b82e GREEN
DeploScheduleRun.java 2b07bd6b40cf4ce2eabc12198f6db3b9655bed25 GREEN
DeploymentRun.java 4b2d0a6d64bb5a6efabc2ee9bf933cc523843ac8 GREEN
EnergyConstraintDefinition.java cc18ecec975ce706ebcb83e282c9a17fe4608596 GREEN
DSMLTransformationService.java 642825f94e172094f7412e9e3e8f7f35414c8228 GREEN
DSMLtoSMTTransformator.java 29663e8526f5c7d3acd85eab4f5609b9f0fcba54 GREEN
DefaultExpressionTransformator.java b890bc609fe9cc45c0af88524ae83cf367ccaee4 GREEN
EnergyConstraintDefinition.java f394e4195ed678ae294b48dbe3c39c783f9c927d GREEN
ExpressionTransformator.java 81dfc30221e519aa8175693353ace8992687327f GREEN
IDSMLTransformationService.java 4c5bd9a06d74e31823bd8ef586687cbb344291e0 GREEN
IDSMLTransformationService.java 0bbcefa52d1127250697ca3d92a1b810db1b8871 GREEN
NonQuantifiedExpressionTransformator.java 9ee437aeaf518d94b81e34a275cd01b87cfca1bf GREEN
QuantifiedExpressionTransformator.java 01e7162b24d16adb23f646cf02340879e8a18205 GREEN
SMTTransformationUtils.java 376da0f5dafb350b49004c7d75fb8858b53d3b7d GREEN
ScheduleRun.java 43d869a9adfbebe34c34f1ebb0bc8e0600f45b9d GREEN
SolverRun.java ff3c69cf4fed2007f7f6bbeaefb4a2343d3c2e8d YELLOW
TimingConstraintDefinition.java 92281277d99bb52b72c1cb898bba944b3b9a24f7 GREEN
......@@ -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(