Skip to content
Snippets Groups Projects
Commit b23fe731 authored by Andreas Bayha's avatar Andreas Bayha
Browse files

Variability: First complete version of optimized Z3 translation 

First complete implementation of EMFProductLineTranslation (optimized
translation for product-line analysis)

Issue-ref: 4240
Issue-Url: af3#4240



Signed-off-by: default avatarAndreas Bayha <bayha@fortiss.org>
parent d840d325
No related branches found
No related tags found
1 merge request!1784240
Pipeline #38574 passed
Stage: test
Pipeline: maven-releng

#38575

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