diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
index a52e72050b205aee17571a3af737ea5f9ad39d07..41d3a1d6e39ea68b67642e65c4650074e7a6ae1c 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
@@ -1,12 +1,10 @@
package org.fortiss.variability.analysis;
import static java.util.stream.Collectors.toList;
-import static org.fortiss.variability.util.VariabilityUtilsInternal.calculateGlobalPresenceCondition;
+import static org.fortiss.variability.model.VariabilityModelElementFactory.createAndPC;
import static org.fortiss.variability.util.VariabilityUtilsInternal.getChildrenWithType;
-import static org.fortiss.variability.util.VariabilityUtilsInternal.getContainedSuperClass;
import java.util.ArrayList;
-import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
@@ -22,7 +20,8 @@ import org.eclipse.emf.ecore.EEnumLiteral;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.EReference;
import org.eclipse.emf.ecore.EcorePackage;
-import org.fortiss.variability.model.IVariationPoint;
+import org.fortiss.variability.model.IAlternative;
+import org.fortiss.variability.model.IOptionalVariationPoint;
import org.fortiss.variability.model.features.AbstractAlternativeFeature;
import org.fortiss.variability.model.features.AbstractCompositionalFeature;
import org.fortiss.variability.model.features.AbstractCrossFeatureConstraint;
@@ -67,20 +66,21 @@ public class EMFProductLineTranslation {
protected BoolSort boolSort;
/** Mapping from classes to all their objects */
- protected BucketSetMap<EClass, EObject> allObjects = new BucketSetMap<EClass, EObject>();
- /** Mapping from classes to all their subclasses */
- protected BucketSetMap<EClass, EClass> allSubclasses = new BucketSetMap<EClass, EClass>();
+ // protected BucketSetMap<EClass, EObject> allObjects = new BucketSetMap<EClass, EObject>();
+ // /** Mapping from classes to all their subclasses */
+ // protected BucketSetMap<EClass, EClass> allSubclasses = new BucketSetMap<EClass, EClass>();
- /** Classes which are not supposed to be translated (usually for optimization). */
- protected Set<EClass> excludedClasses = new HashSet<EClass>();
+ // /** Classes which are not supposed to be translated (usually for optimization). */
+ // protected Set<EClass> excludedClasses = new HashSet<EClass>();
/** References which are not supposed to be translated (usually for optimization). */
- protected Set<EReference> excludedReferences = new HashSet<EReference>();
- /** Mapping from classes to all attributes of the respective type. */
- protected BucketSetMap<EClass, EAttribute> translatedAttributes =
- new BucketSetMap<EClass, EAttribute>();
- /** Mapping from classes to all references of the respective type. */
- protected BucketSetMap<EClass, EReference> translatedReferences =
- new BucketSetMap<EClass, EReference>();
+ // protected Set<EReference> excludedReferences = new HashSet<EReference>();
+ // /** Mapping from classes to all attributes of the respective type. */
+ // protected BucketSetMap<EClass, EAttribute> eClass2TranslatedAttributes =
+ // new BucketSetMap<EClass, EAttribute>();
+ // /** Mapping from classes to all references of the respective type. */
+ // protected BucketSetMap<EClass, EReference> eclass2TranslatedReferences =
+ // new BucketSetMap<EClass, EReference>();
+
/** Mapping of attributes to their translated Z3 function. */
protected DualKeyMap<EAttribute, EClass, FuncDecl> eAttribute2FunDecl =
new DualKeyMap<EAttribute, EClass, FuncDecl>();
@@ -94,7 +94,7 @@ public class EMFProductLineTranslation {
/** Mapping of EDataTypes (e.g. EInt) to their translated Z3 type. */
protected Map<EDataType, Sort> eDataType2Sort = new HashMap<EDataType, Sort>();
/** Mapping for classes to their respective Z3 type. */
- protected Map<EClass, EnumSort> eClass2Datatype = new HashMap<EClass, EnumSort>();
+ protected Map<EClass, EnumSort> eClass2z3Sort = new HashMap<EClass, EnumSort>();
/** Mapping of class.reference to the respective z3 function. */
protected DualKeyMap<EClass, String, FuncDecl> attRefNames2FuncDecl =
@@ -104,7 +104,7 @@ public class EMFProductLineTranslation {
* Mapping of objects with types to their translated Z3 expressions. (EClass is necessary as an
* object is translated for all classes in the inheritance hierarchy).
*/
- protected DualKeyMap<EObject, EClass, Expr> eObject2Expr =
+ protected DualKeyMap<EObject, EClass, Expr> eObject2z3Expr =
new DualKeyMap<EObject, EClass, Expr>();
protected Map<Expr, EObject> expr2EObject = new HashMap<Expr, EObject>();
@@ -134,12 +134,17 @@ public class EMFProductLineTranslation {
/** List of all assertions which encode the presence conditions. */
protected List<BoolExpr> presenceConditionAssertions = new ArrayList<BoolExpr>();
- /* Refacting */
+ /* Refactoring */
+
+ protected Set<EClass> translatedClasses;
+ protected Set<EReference> translatedReferences;
+ protected Set<EAttribute> translatedAttributes;
- protected Set<Class<? extends EObject>> translatedClasses;
- protected Set<EReference> translatedRefernces;
- protected Set<EObject> translatedObjects;
- protected BucketSetMap<Class<? extends EObject>, EObject> class2TranslatedEObjects;
+ protected AbstractFeatureModel featureModel;
+ // protected Set<EObject> translatedObjects;
+ protected BucketSetMap<EClass, EObject> class2TranslatedEObjects;
+
+ protected Map<EObject, PresenceConditionTerm> object2presenceCondition;
/**
* Constructor.
@@ -160,16 +165,19 @@ public class EMFProductLineTranslation {
eDataType2Sort.put(EcorePackage.Literals.ESTRING, stringSort);
eDataType2Sort.put(EcorePackage.Literals.EBOOLEAN, boolSort);
- class2TranslatedEObjects = new BucketSetMap<Class<? extends EObject>, EObject>();
+ translatedClasses = getTranslatedEClasses();
+ translatedReferences = getTranslatedReferences();
+ translatedAttributes = getTranslatedAttributes();
+
+ class2TranslatedEObjects = new BucketSetMap<EClass, EObject>();
+ object2presenceCondition = new HashMap<EObject, PresenceConditionTerm>();
}
/** Performs the complete translation of the product-line to Z3. */
/* package */ void doTranslate(EObject model) {
- // Prepare the core translation
- setTranslatedClassesAndReferences();
+ collectTranslatedObjects(model, null);
- translateFeatureModel(model);
- collectTranslatedObjects(model);
+ translateFeatureModel();
// Metamodel translation
translateClassesMetamodel();
@@ -182,111 +190,194 @@ public class EMFProductLineTranslation {
translateObjects();
}
- /**
- * TODO
- *
- * @param model
- */
- private void collectTranslatedObjects(EObject model) {
+ private void collectTranslatedObjects(EObject model, PresenceConditionTerm parentCondition) {
+ if(model instanceof AbstractFeatureModel) {
+ featureModel = (AbstractFeatureModel)model;
- EList<? extends EObject> varModelElements = getVariableModelElements(model);
- for(EObject eo : varModelElements) {
- Class<? extends EObject> eoClass = eo.getClass();
- if(translatedClasses.contains(eoClass)) {
- collectEObject(eo, eoClass);
+ return;
+ }
- continue;
- }
+ EClass modelClass = model.eClass();
+ PresenceConditionTerm pc = getLocalPresenceCondition(model);
- for(Class<? extends EObject> t : translatedClasses) {
- if(t.isAssignableFrom(eoClass)) {
- collectEObject(eo, t);
+ if(pc == null) {
+ pc = parentCondition;
+ } else {
+ if(parentCondition != null)
+ pc = createAndPC(pc, parentCondition, "");
+ }
+
+ for(EClass cls : translatedClasses) {
+ if(cls.isSuperTypeOf(modelClass)) {
+ // Only optional objects are translated.
+ if(pc != null) {
+ collectEObject(model, cls, pc);
}
}
}
- }
- /**
- * @param eo
- */
- private void collectEObject(EObject eo, Class<? extends EObject> cls) {
- class2TranslatedEObjects.add(cls, eo);
-
- for(EReference ref : eo.eClass().getEAllReferences()) {
- if(translatedRefernces.contains(ref)) {
- Object refTarget = eo.eGet(ref);
- if(refTarget instanceof EObject) {
- EObject refEObj = (EObject)refTarget;
-
- Class<? extends EObject> refClass = refEObj.getClass();
- if(translatedClasses.contains(refClass)) {
- collectEObject(refEObj, refClass);
+ for(EObject child : model.eContents()) {
+ collectTranslatedObjects(child, pc);
+ }
+ }
- continue;
- }
+ private void collectTranslatedReferences(EObject model) {
+ for(EReference ref : model.eClass().getEAllReferences()) {
+ if(translatedReferences.contains(ref)) {
+ EObject refObj = (EObject)model.eGet(ref);
- Class<? extends EObject> translRefCls =
- getContainedSuperClass(refClass, translatedClasses);
- if(translRefCls != null) {
- collectEObject(eo, translRefCls);
- } else {
- throw new RuntimeException("Invalid reference target class found. Class " +
- refClass.getCanonicalName() + " is not translated.");
- }
+ EClass refClass = ref.eClass();
+ if(translatedClasses.contains(refClass)) {
+ class2TranslatedEObjects.add(refClass, refObj);
+ } else {
+ throw new RuntimeException("Invalid reference target class found. Class " +
+ refClass.getName() + " is not translated.");
}
+ collectTranslatedReferences(refObj);
+
}
}
}
/**
* @param model
+ * @return
*/
- protected EList<? extends EObject> getVariableModelElements(EObject model) {
- return getChildrenWithType(model, IVariationPoint.class);
+ private PresenceConditionTerm getLocalPresenceCondition(EObject model) {
+ if(model instanceof IOptionalVariationPoint<?>) {
+ return ((IOptionalVariationPoint<?>)model).getPresenceCondition()
+ .resolveToFeatureLiterals();
+ }
+ if(model instanceof IAlternative) {
+ return ((IAlternative)model).getPresenceCondition().resolveToFeatureLiterals();
+ }
+
+ return null;
}
/**
- * TODO
+ * @param eo
*/
- protected void setTranslatedClassesAndReferences() {
- // EMPTY
+ private void collectEObject(EObject eo, EClass cls, PresenceConditionTerm pc) {
+ class2TranslatedEObjects.add(cls, eo);
+
+ collectTranslatedReferences(eo);
+
+ object2presenceCondition.put(eo, pc);
}
- /** Translates the presence conditions to Z3. */
+ // OLD
+
+ // /**
+ // * TODO
+ // *
+ // * @param model
+ // */
+ // private void collectTranslatedObjects(EObject model) {
+ //
+ // EList<? extends EObject> varModelElements = getVariableModelElements(model);
+ // for(EObject eo : varModelElements) {
+ // Class<? extends EObject> eoClass = eo.getClass();
+ // if(translatedClasses.contains(eoClass)) {
+ // collectEObject(eo, eoClass);
+ //
+ // continue;
+ // }
+ //
+ // for(Class<? extends EObject> t : translatedClasses) {
+ // if(t.isAssignableFrom(eoClass)) {
+ // collectEObject(eo, t);
+ // }
+ // }
+ // }
+ // }
+ //
+ // /**
+ // * @param eo
+ // */
+ // private void collectEObject(EObject eo, Class<? extends EObject> cls) {
+ // class2TranslatedEObjects.add(cls, eo);
+ //
+ // for(EReference ref : eo.eClass().getEAllReferences()) {
+ // if(translatedRefernces.contains(ref)) {
+ // Object refTarget = eo.eGet(ref);
+ // if(refTarget instanceof EObject) {
+ // EObject refEObj = (EObject)refTarget;
+ //
+ // Class<? extends EObject> refClass = refEObj.getClass();
+ // if(translatedClasses.contains(refClass)) {
+ // collectEObject(refEObj, refClass);
+ //
+ // continue;
+ // }
+ //
+ // Class<? extends EObject> translRefCls =
+ // getContainedSuperClass(refClass, translatedClasses);
+ // if(translRefCls != null) {
+ // collectEObject(eo, translRefCls);
+ // } else {
+ // throw new RuntimeException("Invalid reference target class found. Class " +
+ // refClass.getCanonicalName() + " is not translated.");
+ // }
+ // }
+ //
+ // }
+ // }
+ // }
+ //
+ // /**
+ // * @param model
+ // */
+ // protected EList<? extends EObject> getVariableModelElements(EObject model) {
+ // return getChildrenWithType(model, IVariationPoint.class);
+ // }
+
+ protected HashSet<EClass> getTranslatedEClasses() {
+ return new HashSet<EClass>();
+ }
+
+ protected HashSet<EReference> getTranslatedReferences() {
+ return new HashSet<EReference>();
+ }
+
+ protected HashSet<EAttribute> getTranslatedAttributes() {
+ return new HashSet<EAttribute>();
+ }
+
+ /** Translates all presence conditions to Z3. */
protected void translatePresenceConditions() {
- for(EClass ec : allObjects.keySet()) {
- EnumSort ecSort = eClass2Datatype.get(ec);
+ for(EClass ec : class2TranslatedEObjects.keySet()) {
+ EnumSort ecSort = eClass2z3Sort.get(ec);
FuncDecl selFun = ctx.mkFuncDecl("SELECTED_" + ec.getName(), ecSort, boolSort);
eClass2SelectionFunction.put(ec, selFun);
- for(EObject eo : allObjects.get(ec)) {
- BoolExpr eoSelection = eObject2Selection.get(eo);
+ for(EObject eo : class2TranslatedEObjects.get(ec)) {
+ BoolExpr eoSelection;
- // If there is no PC term yet, create one
- if(eoSelection == null) {
- final PresenceConditionTerm globalPC = getGlobalPresenceConditionForEObject(eo);
+ final PresenceConditionTerm globalPC = object2presenceCondition.get(eo);
+ if(globalPC != null) {
eoSelection = translatePresenceCondition(globalPC);
- if(eoSelection == null) {
- eoSelection = ctx.mkTrue();
- }
- eObject2Selection.put(eo, eoSelection);
+ } else {
+ eoSelection = ctx.mkTrue();
}
- Expr eoExpr = eObject2Expr.get(eo, ec);
+ eObject2Selection.put(eo, eoSelection);
+
+ Expr eoExpr = eObject2z3Expr.get(eo, ec);
presenceConditionAssertions.add(ctx.mkEq(ctx.mkApp(selFun, eoExpr), eoSelection));
}
}
}
- /**
- * Calculates the global presence condition for any given {@link EObject}.
- *
- * This method might be overwritten if necessary for custom variation point implementations.
- */
- protected PresenceConditionTerm getGlobalPresenceConditionForEObject(EObject eo) {
- return calculateGlobalPresenceCondition(eo);
- }
+ // /**
+ // * Calculates the global presence condition for any given {@link EObject}.
+ // *
+ // * This method might be overwritten if necessary for custom variation point implementations.
+ // */
+ // protected PresenceConditionTerm getGlobalPresenceConditionForEObject(EObject eo) {
+ // return calculateGlobalPresenceCondition(eo);
+ // }
/** Translates a given {@link PresenceCondition} to Z3. */
private BoolExpr translatePresenceCondition(PresenceCondition pc) {
@@ -327,31 +418,24 @@ public class EMFProductLineTranslation {
return null;
}
- /** Overwrite to exclude classes from the translation for optimization purposes. */
- protected void excludeClassesAndReferences() {
- // EMPTY
- }
+ // /** Overwrite to exclude classes from the translation for optimization purposes. */
+ // protected void excludeClassesAndReferences() {
+ // // EMPTY
+ // }
/** Translates the feature model to Z3. */
- protected void translateFeatureModel(EObject model) {
- // FIXME: Optimize!
- EList<AbstractFeatureModel> featureModels =
- getChildrenWithType(model, AbstractFeatureModel.class);
-
- if(featureModels.size() == 0) {
+ private void translateFeatureModel() {
+ if(featureModel == null) {
return;
}
- // There can only be one FeatureModel in any project.
- AbstractFeatureModel fm = featureModels.get(0);
-
- BoolExpr fmExpr = ctx.mkBoolConst("FEATURE_" + fm.getName());
- featureName2BoolExpr.put(fm.getName(), fmExpr);
+ BoolExpr fmExpr = ctx.mkBoolConst("FEATURE_" + featureModel.getName());
+ featureName2BoolExpr.put(featureModel.getName(), fmExpr);
featureModelAssertions.add(fmExpr);
// Translate all features (including alternatives)
- for(AbstractFeature f : getChildrenWithType(fm, AbstractFeature.class)) {
+ for(AbstractFeature f : getChildrenWithType(featureModel, AbstractFeature.class)) {
String name = f.getName();
String constName = "FEATURE_" + name;
final BoolExpr fExpr = ctx.mkBoolConst(constName.replaceAll("@", "AT"));
@@ -374,7 +458,7 @@ public class EMFProductLineTranslation {
}
// For alternatives also translate the alternative selection criteria
- for(AbstractAlternativeFeature af : getChildrenWithType(fm,
+ for(AbstractAlternativeFeature af : getChildrenWithType(featureModel,
AbstractAlternativeFeature.class)) {
BoolExpr afExpr = featureName2BoolExpr.get(af.getName());
EList<AbstractFeature> as = af.getAlternatives();
@@ -394,7 +478,7 @@ public class EMFProductLineTranslation {
}
// Translate all constraints.
- for(AbstractCrossFeatureConstraint c : getChildrenWithType(fm,
+ for(AbstractCrossFeatureConstraint c : getChildrenWithType(featureModel,
AbstractCrossFeatureConstraint.class)) {
AbstractFeature target = c.getTarget();
AbstractFeature source = (AbstractFeature)c.eContainer();
@@ -468,29 +552,29 @@ public class EMFProductLineTranslation {
/** Translates all objects in the model. */
private void translateObjects() {
// Translate objects by class.
- for(EClass ec : allObjects.keySet()) {
- Set<EObject> Objs = allObjects.get(ec);
+ for(EClass ec : class2TranslatedEObjects.keySet()) {
+ Set<EObject> objs = class2TranslatedEObjects.get(ec);
- Set<EAttribute> attributes = translatedAttributes.get(ec);
- if(attributes != null) {
- for(EAttribute ea : attributes) {
+ EList<EAttribute> attributes = ec.getEAllAttributes();
+ for(EAttribute ea : attributes) {
+ if(translatedAttributes.contains(ea)) {
FuncDecl attFunc = eAttribute2FunDecl.get(ea, ec);
- for(EObject eo : Objs) {
+ for(EObject eo : objs) {
Expr attVal = translateAttributeValue(eo, ea);
BoolExpr attValAssertion =
- ctx.mkEq(ctx.mkApp(attFunc, eObject2Expr.get(eo, ec)), attVal);
+ ctx.mkEq(ctx.mkApp(attFunc, eObject2z3Expr.get(eo, ec)), attVal);
modelAssertions.add(attValAssertion);
}
}
}
- Set<EReference> references = translatedReferences.get(ec);
- if(references != null) {
- for(EReference er : references) {
+ EList<EReference> references = ec.getEAllReferences();
+ for(EReference er : references) {
+ if(translatedReferences.contains(er)) {
FuncDecl refFunc = eReference2FunDecl.get(er, ec);
- for(EObject eo : Objs) {
- Expr eoExpr = eObject2Expr.get(eo, ec);
+ for(EObject eo : objs) {
+ Expr eoExpr = eObject2z3Expr.get(eo, ec);
Expr refVal = translateReferenceValue(eo, er);
BoolExpr rafValAssertion = ctx.mkEq(ctx.mkApp(refFunc, eoExpr), refVal);
modelAssertions.add(rafValAssertion);
@@ -527,15 +611,16 @@ public class EMFProductLineTranslation {
return ctx.mkEmptySeq(eReference2Sort.get(er));
}
- // Remove objects of untranslated objects.
- values = values.stream().filter(o -> !excludedClasses.contains(((EObject)o).eClass()))
- .collect(toList());
+ // // Remove objects of untranslated objects.
+ // values = values.stream().filter(o ->
+ // !excludedClasses.contains(((EObject)o).eClass()))
+ // .collect(toList());
SeqExpr[] seqElems = new SeqExpr[values.size()];
for(int i = 0; i < values.size(); i++) {
Object o = values.get(i);
- Expr elemExpr = eObject2Expr.get((EObject)o, refType);
+ Expr elemExpr = eObject2z3Expr.get((EObject)o, refType);
SeqExpr selectedExpr = ctx.mkUnit(elemExpr);
if(refSelFun != null) {
@@ -560,7 +645,7 @@ public class EMFProductLineTranslation {
return refNullValue;
}
- Expr singleValExpr = eObject2Expr.get((EObject)value, refType);
+ Expr singleValExpr = eObject2z3Expr.get((EObject)value, refType);
if(refSelFun != null) {
// Case with variable target
@@ -573,23 +658,25 @@ public class EMFProductLineTranslation {
return singleValExpr;
}
- /** Creates a function call with the given expression as a parameter. */
- protected Expr createFunctionCallOnExpr(Expr startExpr, String funName, EClass startExprType) {
- FuncDecl fun = attRefNames2FuncDecl.get(startExprType, funName);
- return ctx.mkApp(fun, startExpr);
- }
-
- /**
- * Creates a containment reference between the given expressions, analogly to the containment in
- * EMF.
- */
- protected BoolExpr createContainmentReference(Expr contained, Expr container,
- EClass containerType, String refName) {
- SeqExpr contRefExpr = (SeqExpr)createFunctionCallOnExpr(container, refName, containerType);
- // return ctx.mkAnd(ctx.mkNot(ctx.mkEq(ctx.mkLength(contRefExpr), ctx.mkInt(0))),
- // ctx.mkContains(contRefExpr, ctx.mkUnit(contained)));
- return ctx.mkContains(contRefExpr, ctx.mkUnit(contained));
- }
+ // /** Creates a function call with the given expression as a parameter. */
+ // protected Expr createFunctionCallOnExpr(Expr startExpr, String funName, EClass startExprType)
+ // {
+ // FuncDecl fun = attRefNames2FuncDecl.get(startExprType, funName);
+ // return ctx.mkApp(fun, startExpr);
+ // }
+
+ // /**
+ // * Creates a containment reference between the given expressions, analogly to the containment
+ // in
+ // * EMF.
+ // */
+ // protected BoolExpr createContainmentReference(Expr contained, Expr container,
+ // EClass containerType, String refName) {
+ // SeqExpr contRefExpr = (SeqExpr)createFunctionCallOnExpr(container, refName, containerType);
+ // // return ctx.mkAnd(ctx.mkNot(ctx.mkEq(ctx.mkLength(contRefExpr), ctx.mkInt(0))),
+ // // ctx.mkContains(contRefExpr, ctx.mkUnit(contained)));
+ // return ctx.mkContains(contRefExpr, ctx.mkUnit(contained));
+ // }
/** Translates the given EAttribute value for the given object to Z3. */
private Expr translateAttributeValue(EObject eo, EAttribute ea) {
@@ -603,7 +690,7 @@ public class EMFProductLineTranslation {
SeqExpr[] seqElem = new SeqExpr[values.size()];
for(int i = 0; i < values.size(); i++) {
Object o = values.get(i);
- Expr elemExpr = traslatePrimitiveObject(o, attType);
+ Expr elemExpr = translatePrimitiveObject(o, attType);
seqElem[i] = ctx.mkUnit(elemExpr);
}
@@ -611,11 +698,11 @@ public class EMFProductLineTranslation {
return ctx.mkConcat(seqElem);
}
- return traslatePrimitiveObject(value, attType);
+ return translatePrimitiveObject(value, attType);
}
/** Translates the given object for a primitive type (Enums, Integer, String, Boolean) to Z3. */
- private Expr traslatePrimitiveObject(Object value, EDataType attType) {
+ private Expr translatePrimitiveObject(Object value, EDataType attType) {
// Single value
if(attType.equals(EcorePackage.Literals.EINT)) {
if(value == null) {
@@ -649,120 +736,115 @@ public class EMFProductLineTranslation {
/** Creates functions for all attributes and references of the meta model in Z3. */
private void translateAttributesAndReferencesMetamodel() {
- for(EClass ec : allObjects.keySet()) {
+ for(EClass ec : translatedClasses) {
for(EAttribute ea : ec.getEAllAttributes()) {
- String funId = ec.getName() + "_" + ea.getName();
+ if(translatedAttributes.contains(ea)) {
+ String funId = ec.getName() + "_" + ea.getName();
+
+ EDataType attDataType = ea.getEAttributeType();
+ Sort rangeSort = eDataType2Sort.get(attDataType);
+ if(attDataType instanceof EEnum) {
+ if(rangeSort == null) {
+ rangeSort = translateEnum((EEnum)attDataType);
+ eDataType2Sort.put(attDataType, rangeSort);
+ }
+ }
- EDataType attDataType = ea.getEAttributeType();
- Sort rangeSort = eDataType2Sort.get(attDataType);
- if(attDataType instanceof EEnum) {
if(rangeSort == null) {
- rangeSort = translateEnum((EEnum)attDataType);
- eDataType2Sort.put(attDataType, rangeSort);
+ // Attribute is not translated, as all attribute types except enums are
+ // known.
+ continue;
}
- }
-
- if(rangeSort == null) {
- // Attribute is not translated, as all attribute types except enums are known.
- continue;
- }
- FuncDecl funDecl = ctx.mkFuncDecl(funId, eClass2Datatype.get(ec), rangeSort);
+ FuncDecl funDecl = ctx.mkFuncDecl(funId, eClass2z3Sort.get(ec), rangeSort);
- eAttribute2FunDecl.put(ea, ec, funDecl);
- translatedAttributes.add(ec, ea);
- attRefNames2FuncDecl.put(ec, ea.getName(), funDecl);
+ eAttribute2FunDecl.put(ea, ec, funDecl);
+ // eClass2TranslatedAttributes.add(ec, ea);
+ attRefNames2FuncDecl.put(ec, ea.getName(), funDecl);
+ }
}
+
for(EReference er : ec.getEAllReferences()) {
- String funId = ec.getName() + "_" + er.getName();
+ if(translatedReferences.contains(er)) {
+ String funId = ec.getName() + "_" + er.getName();
- EClass refType = er.getEReferenceType();
+ EClass refType = er.getEReferenceType();
- Sort refSort = eClass2Datatype.get(refType);
- if(refSort == null) {
- if(!isReferenceTranslated(er)) {
- // This is the case in which a custom instance class is specified - those
- // cannot
- // be translated.
- continue;
+ Sort refSort = eClass2z3Sort.get(refType);
+ if(refSort == null) {
+ throw new RuntimeException("Reference " + er.getName() +
+ " shall be translated, but is of type " + refType.getName() +
+ " which is not translated. Add the type to the translated classes to translate this reference.");
}
- refSort = translateSuperType(refType);
- if(refSort == null) {
- // There are no instances of this type...
- continue;
+ if(er.getUpperBound() < 0) {
+ // This is the case of unlimited multiplicity, i.e. lists
+ refSort = ctx.mkSeqSort(refSort);
}
- }
- FuncDecl funDecl;
+ FuncDecl funDecl = ctx.mkFuncDecl(funId, eClass2z3Sort.get(ec), refSort);
- if(er.getUpperBound() < 0) {
- // This is the case of unlimited multiplicity
- refSort = ctx.mkSeqSort(refSort);
+ eReference2Sort.put(er, refSort);
+ eReference2FunDecl.put(er, ec, funDecl);
+ // eclass2TranslatedReferences.add(ec, er);
+ attRefNames2FuncDecl.put(ec, er.getName(), funDecl);
}
-
- funDecl = ctx.mkFuncDecl(funId, eClass2Datatype.get(ec), refSort);
-
- eReference2Sort.put(er, refSort);
- eReference2FunDecl.put(er, ec, funDecl);
- translatedReferences.add(ec, er);
- attRefNames2FuncDecl.put(ec, er.getName(), funDecl);
}
}
}
- /** Checks whether the given reference is supposed to be translated. */
- private boolean isReferenceTranslated(EReference ref) {
- if(excludedReferences.contains(ref)) {
- return false;
- }
-
- EClass refType = ref.getEReferenceType();
- if(excludedClasses.contains(refType)) {
- excludedReferences.add(ref);
- // References to excluded classes not translated.
- return false;
- }
-
- // Only EObjects are translated.
- boolean isTranslated = EObject.class.isAssignableFrom(refType.getInstanceClass());
- return isTranslated;
- }
-
- /**
- * Translates the given superType by adding all objects to it, that belong to
- * subtypes.
- */
- private EnumSort translateSuperType(EClass refType) {
- Set<EClass> subClasses = allSubclasses.get(refType);
- if(subClasses == null) {
- // There are no objects of this class in this case, hence it is not relevant.
- return null;
- }
-
- String typeName = refType.getName();
-
- List<EObject> subClassObjects = new ArrayList<EObject>();
- for(EClass subCls : subClasses) {
- if(excludedClasses.contains(subCls)) {
- // If subclass is excluded, it must not be added here, either.
- continue;
- }
- subClassObjects.addAll(allObjects.get(subCls));
- }
-
- Symbol[] allSymbols = new Symbol[subClassObjects.size()];
- for(int i = 0; i < subClassObjects.size(); i++) {
- StringSymbol symbol = ctx.mkSymbol(typeName + i);
-
- allSymbols[i] = symbol;
- }
-
- EnumSort sort = ctx.mkEnumSort(ctx.mkSymbol(typeName), allSymbols);
- eClass2Datatype.put(refType, sort);
-
- return sort;
- }
+ // /** Checks whether the given reference is supposed to be translated. */
+ // private boolean isReferenceTranslated(EReference ref) {
+ // if(excludedReferences.contains(ref)) {
+ // return false;
+ // }
+ //
+ // EClass refType = ref.getEReferenceType();
+ // if(excludedClasses.contains(refType)) {
+ // excludedReferences.add(ref);
+ // // References to excluded classes not translated.
+ // return false;
+ // }
+ //
+ // // Only EObjects are translated.
+ // boolean isTranslated = EObject.class.isAssignableFrom(refType.getInstanceClass());
+ // return isTranslated;
+ // }
+
+ // /**
+ // * Translates the given superType by adding all objects to it, that belong to
+ // * subtypes.
+ // */
+ // private EnumSort translateSuperType(EClass refType) {
+ // Set<EClass> subClasses = allSubclasses.get(refType);
+ // if(subClasses == null) {
+ // // There are no objects of this class in this case, hence it is not relevant.
+ // return null;
+ // }
+ //
+ // String typeName = refType.getName();
+ //
+ // List<EObject> subClassObjects = new ArrayList<EObject>();
+ // for(EClass subCls : subClasses) {
+ // if(excludedClasses.contains(subCls)) {
+ // // If subclass is excluded, it must not be added here, either.
+ // continue;
+ // }
+ // subClassObjects.addAll(allObjects.get(subCls));
+ // }
+ //
+ // Symbol[] allSymbols = new Symbol[subClassObjects.size()];
+ // for(int i = 0; i < subClassObjects.size(); i++) {
+ // StringSymbol symbol = ctx.mkSymbol(typeName + i);
+ //
+ // allSymbols[i] = symbol;
+ // }
+ //
+ // EnumSort sort = ctx.mkEnumSort(ctx.mkSymbol(typeName), allSymbols);
+ // eClass2Datatype.put(refType, sort);
+ //
+ // return sort;
+ // }
/** Translates the give enumeration */
private Sort translateEnum(EEnum en) {
@@ -790,8 +872,8 @@ public class EMFProductLineTranslation {
/** Creates the types for all classes and objects in Z3. */
private void translateClassesMetamodel() {
- for(EClass cls : allObjects.keySet()) {
- List<EObject> objs = new ArrayList<EObject>(allObjects.get(cls));
+ for(EClass cls : translatedClasses) {
+ List<EObject> objs = new ArrayList<EObject>(class2TranslatedEObjects.get(cls));
// The last index is added for the null element.
Symbol[] objSymbols = new Symbol[objs.size() + 1];
@@ -806,12 +888,12 @@ public class EMFProductLineTranslation {
// Create EnumSort for class
EnumSort enumSort = ctx.mkEnumSort(ctx.mkSymbol(clsName), objSymbols);
- eClass2Datatype.put(cls, enumSort);
+ eClass2z3Sort.put(cls, enumSort);
// Map objects to z3 enum literals
Expr[] consts = enumSort.getConsts();
for(int i = 0; i < objs.size(); i++) {
- eObject2Expr.put(objs.get(i), cls, consts[i]);
+ eObject2z3Expr.put(objs.get(i), cls, consts[i]);
expr2EObject.put(consts[i], objs.get(i));
}
Expr noneExpr = consts[consts.length - 1];
@@ -824,33 +906,34 @@ public class EMFProductLineTranslation {
// FIXME //error(getDefault(), "Error in product-line translation: " + message);
}
- /**
- * Checks whether any of the elements in the given {@link Collection} is contained in the given
- * set of elements.
- *
- * @param set
- * The {@link Set} to check for containment.
- * @param elements
- * The {@link Collection} of elements to be checked for containment in the set.
- *
- * @return 'true' if at least one of the elements on the given {@link Collection} is contained
- * in the given {@link Set}.
- */
- public <E> boolean containsAny(Set<E> set, Collection<E> elements) {
- for(E e : elements) {
- if(set.contains(e)) {
- return true;
- }
- }
- return false;
- }
-
- /**
- * @param clss
- */
- public void addExcludedClasses(Collection<EClass> clss) {
- this.excludedClasses.addAll(clss);
- }
+ // /**
+ // * Checks whether any of the elements in the given {@link Collection} is contained in the
+ // given
+ // * set of elements.
+ // *
+ // * @param set
+ // * The {@link Set} to check for containment.
+ // * @param elements
+ // * The {@link Collection} of elements to be checked for containment in the set.
+ // *
+ // * @return 'true' if at least one of the elements on the given {@link Collection} is contained
+ // * in the given {@link Set}.
+ // */
+ // public <E> boolean containsAny(Set<E> set, Collection<E> elements) {
+ // for(E e : elements) {
+ // if(set.contains(e)) {
+ // return true;
+ // }
+ // }
+ // return false;
+ // }
+
+ // /**
+ // * @param clss
+ // */
+ // public void addExcludedClasses(Collection<EClass> clss) {
+ // this.excludedClasses.addAll(clss);
+ // }
/** Returns ctx. */
public Context getContext() {
@@ -861,32 +944,32 @@ public class EMFProductLineTranslation {
public Map<EClass, Expr> getEClass2NullElement() {
return eClass2NullElement;
}
-
- /** Traverses the model to collect all classes and objects to be translated. */
- private void collectClassesAndObjectsRecrsively(EObject model) {
- EClass eClass = model.eClass();
- EList<EClass> superTypes = eClass.getEAllSuperTypes();
-
- if(excludedClasses.contains(eClass)) {
- return;
- }
-
- if(containsAny(excludedClasses, superTypes)) {
- excludedClasses.add(eClass);
- return;
- }
-
- for(EClass sprCls : superTypes) {
- if(!sprCls.equals(EcorePackage.Literals.EOBJECT)) {
- allObjects.add(sprCls, model);
- allSubclasses.add(sprCls, eClass);
- }
- }
-
- allObjects.add(eClass, model);
-
- for(EObject c : model.eContents()) {
- collectClassesAndObjectsRecrsively(c);
- }
- }
+ //
+ // /** Traverses the model to collect all classes and objects to be translated. */
+ // private void collectClassesAndObjectsRecrsively(EObject model) {
+ // EClass eClass = model.eClass();
+ // EList<EClass> superTypes = eClass.getEAllSuperTypes();
+ //
+ // if(excludedClasses.contains(eClass)) {
+ // return;
+ // }
+ //
+ // if(containsAny(excludedClasses, superTypes)) {
+ // excludedClasses.add(eClass);
+ // return;
+ // }
+ //
+ // for(EClass sprCls : superTypes) {
+ // if(!sprCls.equals(EcorePackage.Literals.EOBJECT)) {
+ // allObjects.add(sprCls, model);
+ // allSubclasses.add(sprCls, eClass);
+ // }
+ // }
+ //
+ // allObjects.add(eClass, model);
+ //
+ // for(EObject c : model.eContents()) {
+ // collectClassesAndObjectsRecrsively(c);
+ // }
+ // }
}