Commit 1e11ed7c authored by Tiziano Munaro's avatar Tiziano Munaro

DSE: Adapt models to the per-quantifier unfolding

Issue-Ref: 3766
Issue-Url: https://af3-developer.fortiss.org/issues/3766Signed-off-by: Tiziano Munaro's avatarTiziano Munaro <munaro@fortiss.org>
parent 7c6f0286
model.ecore e3ae1bda40b05a075470fbcf0a856b9e38d2f265 GREEN
model.ecore ec3a8b404acef40f7198b5e68628759fc99cd724 YELLOW
......@@ -5,12 +5,6 @@
<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."/>
</eAnnotations>
<eStructuralFeatures xsi:type="ecore:EAttribute" name="unfoldQuantifier" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBoolean"
defaultValueLiteral="true">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
<details key="documentation" value="If this constraint contains a quantifier, this flag states if the constraint shall be unfolded manually in the transformation to SMT."/>
</eAnnotations>
</eStructuralFeatures>
<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"/>
</eGenericSuperTypes>
......
......@@ -9,9 +9,7 @@
<foreignModel>model.ecore</foreignModel>
<genPackages prefix="AF3ExplorationSMT" basePackage="org.fortiss.af3.exploration.smt"
disposableProviderFactory="true" ecorePackage="model.ecore#/">
<genClasses ecoreClass="model.ecore#//SMTConstraint">
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute model.ecore#//SMTConstraint/unfoldQuantifier"/>
</genClasses>
<genClasses ecoreClass="model.ecore#//SMTConstraint"/>
<genClasses ecoreClass="model.ecore#//SMTObjective">
<genFeatures notify="false" createChild="false" propertySortChoices="true" ecoreFeature="ecore:EReference model.ecore#//SMTObjective/constraints"/>
</genClasses>
......
BasicDeploScheduleConstraint.java 6fa1f1063a83ed6b94c9063d3e27c91a5ffeea54 GREEN
BasicDeploymentConstraint.java 32e308d50529144b306866c82cbf03fba75e1413 GREEN
BasicDeploScheduleConstraint.java 2570262c18ad57e0843f600da389031e3eec053d RED
BasicDeploymentConstraint.java df8d1faedc695e8d3a0b560856dca0e7efad9f98 RED
BasicScheduleConstraint.java 618ec93bfe626c600dd25b530009966fcbd1497a GREEN
ConstraintDefinitionUtils.java 67ca9b73b8edccf0dbfccf1a761d11d9f48b49b7 GREEN
ConstraintToNonQuantifiedSMT.java ab629ab1e75d35874362d9068e1ee8bf485b0318 GREEN
ConstraintToQuantifiedSMT.java dcea10daf55b60cdadd875fa87a132e753b52b34 GREEN
DSMLTransformationService.java 5d296af2d43faf1d6765945489164f653eaab513 GREEN
DSMLtoSMTTransformator.java 2c87c5f44a8a61368c0e502334276bab2a7de1b6 GREEN
DSMLtoSMTTransformator.java 5811bfeb43072d2af3180a4be9d9a198ad83e139 RED
DeploScheduleRun.java 3ff8b67260d752ef5cccfd22def13b73752e8f52 GREEN
DeploymentRun.java ba491feb02e0b2790dc4e2777f88d45776d5382e GREEN
IDSMLTransformationService.java d02a25d050c52b83041021323e5720775c1248ba GREEN
......
......@@ -124,8 +124,7 @@ public class BasicDeploScheduleConstraint {
assertions.addAll(createCausalityConstraints(resAllocSS, taskSS, signalSS, ecuSS));
int i = 0;
for(IBooleanExpression a : assertions) {
SMTConstraint ts =
createSMTConstraint("Implicit Schedule Constraint " + i++, a, true, false);
SMTConstraint ts = createSMTConstraint("Implicit Schedule Constraint " + i++, a, true);
generatedConstraints.add(ts);
prepareUniqueID(ts, fileProject);
}
......
......@@ -188,7 +188,7 @@ public class BasicDeploymentConstraint {
Implies implies = createImplies(allocationCH_Route, createAnd);
forAllRoutes.setExpression(implies);
return createSMTConstraint("Basic Deployment Constraint", forAllCH, true, false);
return createSMTConstraint("Basic Deployment Constraint", forAllCH, true);
}
/** Creates an {@link Start} literal. */
......@@ -245,7 +245,7 @@ public class BasicDeploymentConstraint {
Equal equals = cmpFnc.apply(channelsModelElementSet, tasksModelElementSet);
forAllComp.setExpression(equals);
return createSMTConstraint(constraintName, forAllCH, true, true);
return createSMTConstraint(constraintName, forAllCH, true);
}
/** Creates start and end constraints of {@link IConnection}s. */
......
......@@ -50,7 +50,6 @@ import org.eclipse.emf.common.util.Enumerator;
import org.fortiss.af3.exploration.dseml.model.arithmetic.IArithmeticExpression;
import org.fortiss.af3.exploration.dseml.model.arithmetic.ModelElementPropertyLiteral;
import org.fortiss.af3.exploration.dseml.model.booleanp.ForAll;
import org.fortiss.af3.exploration.dseml.model.booleanp.IBooleanExpression;
import org.fortiss.af3.exploration.dseml.model.expression.IBinderExpression;
import org.fortiss.af3.exploration.dseml.model.expression.IExpression;
import org.fortiss.af3.exploration.dseml.model.expression.Set;
......@@ -110,7 +109,7 @@ public class DSMLtoSMTTransformator {
/** Basic transformation. */
private ConstraintToQuantifiedSMT basicQuantifiedTransformation;
/** Basic non quantfied transformation. */
/** Basic non quantified transformation. */
private ConstraintToNonQuantifiedSMT genericNonQuantifiedTransformation;
/** Transformation Service instance to be used. */
......@@ -346,14 +345,8 @@ public class DSMLtoSMTTransformator {
/** Extracts the respective SMT expression by translating the given {@link SMTConstraint}. */
private Expr extractSMTExpr(SMTConstraint constraint) throws UnsupportedDataTypeException {
IExpression expression = constraint.getExpression();
Expr smt;
if(!constraint.isUnfoldQuantifier()) {
smt = basicQuantifiedTransformation.toSMT(expression);
} else {
// quantifiers get unfolded
smt = genericNonQuantifiedTransformation.transfrom((IBooleanExpression)expression);
}
Expr smt = basicQuantifiedTransformation.toSMT(constraint.getExpression());
if(!constraint.isImplicit()) {
constraintsToTrack.add((BoolExpr)smt);
}
......
AllocationToSchedule.java 9820c41b6a2a804306b41fd2e7defabd37fb710e GREEN
ResourceConnection.java b0a3a5ad48e90729d06bb89aaa90759eb437fdc3 GREEN
RouteUtils.java 0da07aff213eb0f62420f790b1aa9f7d2c4b975a GREEN
Z3ModelElementFactory.java cb49d1d360f547df120dd9719c12e00c671477df GREEN
Z3ModelElementFactory.java 700aa6c09240380af36d034ca9da4553370f2a64 YELLOW
......@@ -37,17 +37,6 @@ public class Z3ModelElementFactory {
return testConstraint;
}
/** Creates a SMT Constraint. */
public static SMTConstraint createSMTConstraint(String name, IExpression expression,
boolean isImplicit, boolean unfoldQuantifier) {
SMTConstraint testConstraint = AF3ExplorationSMTFactory.eINSTANCE.createSMTConstraint();
testConstraint.setExpression(expression);
testConstraint.setName(name);
testConstraint.setImplicit(isImplicit);
testConstraint.setUnfoldQuantifier(unfoldQuantifier);
return testConstraint;
}
/** Creates a SMT Constraint. */
public static SMTConstraint createSMTConstraint() {
return AF3ExplorationSMTFactory.eINSTANCE.createSMTConstraint();
......
BusBandwidthOptimizationBackend.java ca4119c873e3a0895d4c6a5f06cc633d3a2da00d GREEN
BusBandwidthOptimizationBackend.java 0c5dfb93dcee56b1468b60b14c47f3f3cb229186 RED
BusEliminationBackend.java 847a39f6ae36e75d12eafeb55cff385970a3a09c GREEN
HardwareOptimizationPatternCompositeBackend.java 664e7e53ec178c94cfd591734ea6be3a4fd70f9e GREEN
ObjectiveViewBackend.java 67ee646b34e06b28babf0ed6cb0c0de4690a9d12 GREEN
......@@ -200,7 +200,7 @@ public class BusBandwidthOptimizationBackend extends BusBandwidthOptimzationPatt
forAllRoute.setExpression(equals);
SMTConstraint smtConstraint =
createSMTConstraint("BandwidthWeight_forAllRoutes", forAllRoute, true, false);
createSMTConstraint("BandwidthWeight_forAllRoutes", forAllRoute, true);
results.add(smtConstraint);
return results;
......@@ -238,7 +238,7 @@ public class BusBandwidthOptimizationBackend extends BusBandwidthOptimzationPatt
Equal createEquals = createEquals(createUses, literal);
forAll2.setExpression(createEquals);
SMTConstraint smtConstraint =
createSMTConstraint("VirtualLinkUsesBus", forAll1, true, true);
createSMTConstraint("VirtualLinkUsesBus", forAll1, true);
results.add(smtConstraint);
}
}
......
dseml.ecore 67b3df06878185c2a69305224d1efacf4c942996 GREEN
dseml.ecore 8e85999e8e556e84e1479643c27ba4185e6ab58e YELLOW
exploration.ecore 80f1561f9575c41e06785a165d1f77325de1db35 GREEN
......@@ -318,6 +318,12 @@
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
<details key="documentation" value="TODO: write documentation (in the model!)"/>
</eAnnotations>
<eStructuralFeatures xsi:type="ecore:EAttribute" name="unfold" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EBoolean"
defaultValueLiteral="false">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
<details key="documentation" value="This flag states whether the quantifier shall be unfolded in the transformation to SMT."/>
</eAnnotations>
</eStructuralFeatures>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="ForAll" eSuperTypes="#//booleanp/IQuantifierExpression">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
......
......@@ -106,7 +106,9 @@
<genParameters ecoreParameter="dseml.ecore#//booleanp/BooleanLiteral/equals/other"/>
</genOperations>
</genClasses>
<genClasses image="false" ecoreClass="dseml.ecore#//booleanp/IQuantifierExpression"/>
<genClasses image="false" ecoreClass="dseml.ecore#//booleanp/IQuantifierExpression">
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute dseml.ecore#//booleanp/IQuantifierExpression/unfold"/>
</genClasses>
<genClasses ecoreClass="dseml.ecore#//booleanp/ForAll">
<genOperations ecoreOperation="dseml.ecore#//booleanp/ForAll/toString" body="return org.fortiss.af3.exploration.model.booleanp.impl.BooleanpStaticImpl.toString(this);"/>
<genOperations ecoreOperation="dseml.ecore#//booleanp/ForAll/equals" body="return org.fortiss.af3.exploration.model.booleanp.impl.BooleanpStaticImpl.equals(this, other);">
......@@ -206,14 +208,12 @@
<genClasses ecoreClass="dseml.ecore#//function/Maximize">
<genFeatures notify="false" createChild="false" propertySortChoices="true"
ecoreFeature="ecore:EReference dseml.ecore#//function/Maximize/args"/>
<genOperations ecoreOperation="dseml.ecore#//function/Maximize/toString"
body="return org.fortiss.af3.exploration.model.function.FunctionStaticImpl.toString(this);"/>
<genOperations ecoreOperation="dseml.ecore#//function/Maximize/toString" body="return org.fortiss.af3.exploration.model.function.FunctionStaticImpl.toString(this);"/>
</genClasses>
<genClasses ecoreClass="dseml.ecore#//function/Minimize">
<genFeatures notify="false" createChild="false" propertySortChoices="true"
ecoreFeature="ecore:EReference dseml.ecore#//function/Minimize/args"/>
<genOperations ecoreOperation="dseml.ecore#//function/Minimize/toString"
body="return org.fortiss.af3.exploration.model.function.FunctionStaticImpl.toString(this);"/>
<genOperations ecoreOperation="dseml.ecore#//function/Minimize/toString" body="return org.fortiss.af3.exploration.model.function.FunctionStaticImpl.toString(this);"/>
</genClasses>
<genClasses ecoreClass="dseml.ecore#//function/Start">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference dseml.ecore#//function/Start/args"/>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment