Skip to content
GitLab
Commit 7c7b092f authored by Johannes Eder's avatar Johannes Eder
Browse files

Merge branch 'master' into 4022 



Conflicts:
	org.fortiss.af3.exploration.ui/src/org/fortiss/af3/exploration/ui/perspective/dashboard/projectwizard/.ratings
	org.fortiss.af3.exploration.ui/src/org/fortiss/af3/exploration/ui/perspective/dashboard/projectwizard/DashboardWizardSelectPlatformArchitecture.java
	org.fortiss.af3.exploration.ui/src/org/fortiss/af3/exploration/ui/perspective/targetdef/constraint/pattern/.ratings
	org.fortiss.af3.exploration.ui/src/org/fortiss/af3/exploration/ui/perspective/targetdef/constraint/pattern/SafetyPatternFXController.java
Signed-off-by: Johannes Eder's avatarJohannes Eder <eder@fortiss.org>
parents d8dbc962 7c7c6d67
Hide whitespace changes
Inline Side-by-side
com.microsoft.z3/src/com/microsoft/z3/.ratings
View file @ 7c7b092f
AF3z3Activator.java 3b41854f824afc76c3f804e627ca24dc438df758 GREEN
Z3Type.java 73e319ae206d2fd456ec9430c01b5ff7fc7282d0 GREEN
Z3javaAPIWrapper.java d21fa89f50dd9afe49eaad0901384bdf99df548f GREEN
Z3javaAPIWrapper.java 563486b7205451cdb994e8aed70667f04b37239b GREEN
com.microsoft.z3/src/com/microsoft/z3/Z3javaAPIWrapper.java
View file @ 7c7b092f
......@@ -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);
}
......
org.fortiss.af3.exploration.smt/META-INF/MANIFEST.MF
View file @ 7c7b092f
......@@ -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/.ratings
View file @ 7c7b092f
AF3ExplorationSMTActivator.java 499ee7e7485e622615a4f78be5d2e4f1ca8f235a GREEN
AF3ExplorationSMTActivator.java db8c07de55429ead58b5127affc48232e31819d3 YELLOW
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/AF3ExplorationSMTActivator.java
View file @ 7c7b092f
......@@ -16,6 +16,8 @@
package org.fortiss.af3.exploration.smt;
import org.eclipse.core.runtime.Plugin;
import org.fortiss.af3.exploration.smt.cli.DumpSMTLibFileCommandLineHandler;
import org.fortiss.tooling.kernel.service.ICommandLineInterfaceService;
import org.osgi.framework.BundleContext;
/**
......@@ -36,6 +38,9 @@ public class AF3ExplorationSMTActivator extends Plugin {
public void start(BundleContext context) throws Exception {
super.start(context);
plugin = this;
ICommandLineInterfaceService cliService = ICommandLineInterfaceService.getInstance();
cliService.registerHandler("--dump-smtlib", new DumpSMTLibFileCommandLineHandler());
}
/** {@inheritDoc} */
......
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/backend/.ratings
View file @ 7c7b092f
Z3Backend.java 070f627218b36e50f61c56d850d0679e5a69d332 GREEN
Z3Backend.java c217750b1183c51c4f4952919d70e22b2576d7fa GREEN
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/backend/Z3Backend.java
View file @ 7c7b092f
......@@ -15,42 +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.service.DSESolutionVisualization;
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,8 +50,9 @@ import org.fortiss.tooling.base.model.element.IModelElement;
* @author diewald
*/
public class Z3Backend implements IDSEBackend {
/** Caches the solution container (metrics/visualization + solution models). */
private DSESolutionVisualization solutionVisualization;
/** Default timeout value in ms. */
private static int DEFAULT_TIMEOUT = 50 * 1000;
/** {@inheritDoc} */
@Override
......@@ -71,85 +62,32 @@ 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();
List<IExplorationTarget<?>> basicConstraints = new ArrayList<>();
SuperSetMap superSets = spec.getSearchSpace();
SolverRun solverRun;
if(solutionTypes.contains(TaskToExecutionUnitAllocationTable.class)) {
// Add SMT-specific constraints to define the basic deployment problem.
basicConstraints.addAll(createBasicSignalConstraints(superSets));
public Set<EXPLORATION_TYPE> getExplorationTypes() {
return newHashSet(FEASIBILITY_CHECK, OPTIMIZATION);
}
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();
}
} 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);
/** {@inheritDoc} */
@Override
public SolverSettings getSolverSettings() {
return createSolverSettings(DEFAULT_TIMEOUT, 0);
}
if(spec.getTargets().isEmpty()) {
throw new Exception("No exploration targets defined. Cannot perform DSE.");
}
/** {@inheritDoc} */
@Override
public Optional<ExplorationSolution> executeDSE(ExplorationSpecification spec,
SolverSettings settings, IProgressMonitor monitor) throws Exception {
int timeout = settings.getTermination().getTimeoutMS().getValue();
SolverRun solverRun = createSolverRun(spec, timeout);
if(isDebugVerboseEnabled()) {
// prints on screen the list of constraints for this run
......@@ -161,19 +99,28 @@ 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);
}
/** Returns the cached solution representation (metrics/visualization + solution models). */
public DSESolutionVisualization getSolutionVisualization() {
return solutionVisualization;
/**
* Creates a {@link SolverRun} instance that is specific for the {@link ISynthesisCategory}s of
* the given {@link ExplorationSpecification}.
*/
public SolverRun createSolverRun(ExplorationSpecification spec, int timeout) throws Exception {
Collection<Class<? extends ISynthesisCategory>> synthTypes = spec.getSynthTypes();
if(synthTypes.contains(IDeploymentSynthesis.class) &&
synthTypes.contains(IScheduleSynthesis.class)) {
return new DeploScheduleRun(spec, timeout);
} else if(synthTypes.contains(IDeploymentSynthesis.class)) {
return new DeploymentRun(spec, timeout);
} else if(synthTypes.contains(IScheduleSynthesis.class)) {
return new ScheduleRun(spec, timeout);
} else {
throw new Exception("No applicable " + SolverRun.class.getSimpleName() +
" was found for the given set of syntesises to perform.");
}
}
/** {@inheritDoc} */
......
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/cli/.ratings 0 → 100644
View file @ 7c7b092f
DumpSMTLibFileCommandLineHandler.java 95604962b4db14786ec8143663278c4a865bbd55 GREEN
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/cli/DumpSMTLibFileCommandLineHandler.java 0 → 100644
View file @ 7c7b092f
/*-------------------------------------------------------------------------+
| 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.cli;
import static org.fortiss.af3.exploration.service.IDSEBackend.EXPLORATION_TYPE.FEASIBILITY_CHECK;
import static org.fortiss.af3.exploration.util.ExplorationCLIUtils.findMatchingDSEProject;
import static org.fortiss.af3.exploration.util.ExplorationCLIUtils.getExplorationTypeByArgument;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationSpecification;
import static org.fortiss.tooling.common.util.LambdaUtils.getFirst;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getFirstParentWithType;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.pickInstanceOf;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.info;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
import org.fortiss.af3.exploration.AF3ExplorationActivator;
import org.fortiss.af3.exploration.model.ExplorationSpecification;
import org.fortiss.af3.exploration.model.IExplorationConstraint;
import org.fortiss.af3.exploration.model.IExplorationObjective;
import org.fortiss.af3.exploration.model.IExplorationTarget;
import org.fortiss.af3.exploration.model.SolverSettings;
import org.fortiss.af3.exploration.model.project.DSE;
import org.fortiss.af3.exploration.model.project.ProcessStep;
import org.fortiss.af3.exploration.model.project.RuleSet;
import org.fortiss.af3.exploration.model.synthesiscategory.ISynthesisCategory;
import org.fortiss.af3.exploration.service.IDSEBackend;
import org.fortiss.af3.exploration.service.IDSEBackendService;
import org.fortiss.af3.exploration.smt.AF3ExplorationSMTActivator;
import org.fortiss.af3.exploration.smt.backend.Z3Backend;
import org.fortiss.af3.exploration.smt.solver.SolverRun;
import org.fortiss.af3.project.model.FileProject;
import org.fortiss.tooling.kernel.extension.ICommandLineSwitchHandler;
import com.microsoft.z3.Solver;
/**
* Handler to dump a SMT-Lib description of and exploration problem defined in a {@link DSE}
* project. To construct the {@link ExplorationSpecification} that is optimized, all defined
* {@link IExplorationConstraint}s matching the synthesis type are used.
* This handler supports only the generation of feasibility checks. It is intended to be used with
* solvers that support the SMT-Lib standard 2.5 such as CVC4.
*
* @author diewald
*/
public final class DumpSMTLibFileCommandLineHandler implements ICommandLineSwitchHandler {
/** DSE service used for the exploration. */
private final IDSEBackendService dseService = IDSEBackendService.getInstance();
/** {@inheritDoc} */
@Override
public boolean hasAdditionalArgument() {
return true;
}
/** {@inheritDoc} */
@Override
public void handleCLISwitch(String argument) {
DSE matchingDSE = findMatchingDSEProject(argument);
if(matchingDSE == null) {
return;
}
Set<Class<? extends ISynthesisCategory>> solutionType =
getExplorationTypeByArgument(argument);
if(solutionType.isEmpty()) {
return;
}
// Get & set the Z3 solver.
Optional<IDSEBackend> optBackend = getFirst(
dseService.findBySynthTypeAndName(solutionType, FEASIBILITY_CHECK, "Z3 (SMT)"));
if(!optBackend.isPresent()) {
error(AF3ExplorationActivator.getDefault(),
"Could not find the Z3 backend to perform the exploration.");
return;
}
Z3Backend z3Backend = (Z3Backend)optBackend.get();
Map<IDSEBackend, SolverSettings> settings = new HashMap<>();
settings.put(z3Backend, z3Backend.getSolverSettings());
ExplorationSpecification expSpec = constructExplorationSpecification(matchingDSE);
expSpec.getSynthTypes().addAll(solutionType);
SolverRun solverRun;
try {
solverRun = z3Backend.createSolverRun(expSpec, 1000);
} catch(Exception e) {
error(AF3ExplorationActivator.getDefault(),
"Could not create a solver run instance for the given synthesis type.", e);
return;
}
int numExplorationObjectives =
pickInstanceOf(IExplorationObjective.class, expSpec.getTargets()).size();
if(numExplorationObjectives > 0) {
info(AF3ExplorationSMTActivator.getDefault(),
"Optimization statements will not be " +
"dumped. This switch is only inteded to check feasibility of an " +
"optimization problem. For debugging optimization problems, set " +
"the environment varaible DSE_DEBUG_VERBOSE to \"true\".");
}
Solver solver = solverRun.createConstraintSolver();
String smtLibStr = "(set-logic ALL)\n" + "(check-sat)\n" + solver.toString();
String af3PrjName = getFirstParentWithType(matchingDSE, FileProject.class).getName();
solverRun.dumpSMTLibFile(smtLibStr, af3PrjName);
}
/**
* Constructs an {@link ExplorationSpecification} using all {@link IExplorationTarget}s from the
* given {@link DSE}.
*/
private ExplorationSpecification constructExplorationSpecification(DSE matchingDSE) {
ExplorationSpecification expSpec = createExplorationSpecification();
ProcessStep dseStep = matchingDSE.getCurrentStep();
expSpec.getTargets().addAll(getTargetsFromRuleSets(matchingDSE));
expSpec.setSearchSpace(dseStep.getSuperSetMap());
return expSpec;
}
/** Collects all targets referenced by {@link RuleSet}s of the given {@link DSE}. */
private static Collection<IExplorationTarget<?>> getTargetsFromRuleSets(DSE dse) {
Collection<IExplorationTarget<?>> allExplorationTargets = new ArrayList<>();
ProcessStep dseStep = dse.getCurrentStep();
for(RuleSet ruleSet : dseStep.getRuleSets()) {
allExplorationTargets = ruleSet.getExplorationTargets();
}
return allExplorationTargets;
}
}
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/migrate/.ratings
View file @ 7c7b092f
SMTExplorationTargetMigrator.java 843c5e4b8ddb7ddb1ca6f670da6b3d3bb839fe88 GREEN
SMTExplorationTargetMigrator.java c5cf1a5f40ea0a3c1b0940bdbb57950584d44af6 GREEN
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/migrate/SMTExplorationTargetMigrator.java
View file @ 7c7b092f
......@@ -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 @ 7c7b092f
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 5de3aed222e049b2990308a1294b468cef6e35bf 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 be9794b2be0fd203a31435548abe9d9945bc2160 GREEN
TimingConstraintDefinition.java 92281277d99bb52b72c1cb898bba944b3b9a24f7 GREEN
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/modeltransformation/BasicDeploScheduleConstraint.java
View file @ 7c7b092f
......@@ -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;