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

Variability: Removed deprecated old PL-Analysis 

Removed the old, deprecated product-line analysis which is no longer
used.

Issue-ref: 4328
Issue-URL: af3#4328



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

#39340

    Hide whitespace changes
    Inline Side-by-side
    Showing
    with 0 additions and 1090 deletions
    org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/.ratings
    + 0
    − 2
    View file @ c1bf57af
    OptimizedProductLineAnalysisBase.java 35a40c860cc8a9774a894600935c1ae89a5681a0 GREEN
    OptimizedProductLineTranslation.java 415361dd35a04db219b06a1e40079452d7079b34 GREEN
    ProductLineAnalysisBase.java 891235573a2102279256585f8dc31934240b8dc1 GREEN
    ProductLineTranslationBase.java f24fb9343003c025bc4d2292d15bca543a548749 GREEN
    org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineAnalysisBase.java deleted 100644 → 0
    + 0
    − 96
    View file @ 124a12d5
    /*-------------------------------------------------------------------------+
    | Copyright 2022 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.tooling.ext.variability.analysis;
    import static java.util.Arrays.asList;
    import static org.fortiss.tooling.kernel.utils.EcoreUtils.pickInstanceOf;
    import java.util.ArrayList;
    import java.util.Collection;
    import java.util.List;
    import org.eclipse.emf.ecore.EClass;
    import org.eclipse.emf.ecore.EObject;
    import org.fortiss.tooling.base.model.layout.LayoutPackage;
    import org.fortiss.tooling.kernel.model.IProjectRootElement;
    import org.fortiss.variability.analysis.GenericProductLineAnalysis;
    import org.fortiss.variability.analysis.GenericProductLineTranslation;
    import org.fortiss.variability.analysis.ProductLineConstraintViolation;
    /**
    * Base class for all tooling kernel based product-line analyses.
    *
    * @deprecated
    *
    * TODO: To be removed completely #4328 (https://git.fortiss.org/af3/af3/-/issues/4328)
    *
    * @author bayha
    */
    public abstract class ProductLineAnalysisBase extends GenericProductLineAnalysis {
    /**
    * Constructor.
    */
    public ProductLineAnalysisBase(EObject model) {
    this(model, new ProductLineTranslationBase());
    ((ProductLineTranslationBase)translation)
    .addExcludedClasses(asList(LayoutPackage.eINSTANCE.getILayoutData()));
    }
    /**
    * Constructor.
    */
    protected ProductLineAnalysisBase(EObject model, GenericProductLineTranslation translation) {
    super(model, translation);
    }
    /** {@inheritDoc} */
    @Override
    public List<ProductLineConstraintViolation> doCheck() {
    List<Class<? extends IProjectRootElement>> scope = getScope();
    Collection<EClass> excludedClasses = new ArrayList<EClass>();
    for(IProjectRootElement rootElement : pickInstanceOf(IProjectRootElement.class,
    model.eContents())) {
    for(Class<?> c : scope) {
    if(!c.isAssignableFrom(rootElement.getClass())) {
    excludedClasses.add(rootElement.eClass());
    }
    }
    }
    ((ProductLineTranslationBase)translation).addExcludedClasses(excludedClasses);
    return super.doCheck();
    }
    /**
    * Determines the scope of this analysis. I.e. which subclasses of {@link IProjectRootElement}
    * are translated and included to the check.
    *
    * The default implementation will translate all {@link IProjectRootElement}.
    * This method might be overwritten in order to optimize the analysis and runtime.
    *
    * @return A {@link List} of {@link Class} elements for subclasses of
    * {@link IProjectRootElement}.
    */
    protected List<Class<? extends IProjectRootElement>> getScope() {
    return asList(IProjectRootElement.class);
    }
    }
    org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineTranslationBase.java deleted 100644 → 0
    + 0
    − 42
    View file @ 124a12d5
    /*-------------------------------------------------------------------------+
    | Copyright 2022 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.tooling.ext.variability.analysis;
    import static org.fortiss.tooling.ext.variability.util.VariabilityUtils.calculateGlobalPresenceCondition;
    import org.eclipse.emf.ecore.EObject;
    import org.fortiss.tooling.base.model.element.IModelElementSpecification;
    import org.fortiss.variability.analysis.GenericProductLineTranslation;
    import org.fortiss.variability.model.presence.PresenceConditionTerm;
    /**
    * Adjusts the generic implementation of the translation to the variation point translation with
    * {@link IModelElementSpecification}s.
    *
    * @deprecated
    *
    * TODO: To be removed completely #4328 (https://git.fortiss.org/af3/af3/-/issues/4328)
    *
    * @author bayha
    */
    public class ProductLineTranslationBase extends GenericProductLineTranslation {
    /** {@inheritDoc} */
    @Override
    protected PresenceConditionTerm getGlobalPresenceConditionForEObject(EObject eo) {
    return calculateGlobalPresenceCondition(eo);
    }
    }
    org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings
    + 0
    − 1
    View file @ c1bf57af
    ......@@ -2,7 +2,6 @@ BucketSetMap.java 665a28c80a9693b9b9e31b7ebe59f2de4195d56c GREEN
    DualKeyMap.java 75fbe85a54e5a655aaf67108ae004f98ed2879d8 GREEN
    EMFProductLineTranslation.java b590fbf053c21d9e6b0ee6d0818779e4adb1fe0b GREEN
    GenericProductLineAnalysis.java 1026cd6d7d0286c0f2402c5918d83cf7dc84407b GREEN
    GenericProductLineTranslation.java 2df1a1c1363cb93b6f498308e575833cf705e2fd GREEN
    IProductLineConstraint.java 1b0e1231cc578a6e7e544441ac33533b4feafeb1 GREEN
    IProductLineTranslation.java 733dae03e2baae237b6f0b33f0dd618a4f47cf73 GREEN
    ProductLineConstraintBase.java 04097c7c31367fdd11a054ba2b259a0535a313f4 GREEN
    ......
    org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineTranslation.java deleted 100644 → 0
    + 0
    − 949
    View file @ 124a12d5
    package org.fortiss.variability.analysis;
    import static java.util.stream.Collectors.toList;
    import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
    import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
    import static org.fortiss.variability.VariabilityActivator.getDefault;
    import static org.fortiss.variability.util.VariabilityUtilsInternal.calculateGlobalPresenceCondition;
    import java.util.ArrayList;
    import java.util.Collection;
    import java.util.HashMap;
    import java.util.HashSet;
    import java.util.List;
    import java.util.Map;
    import java.util.Set;
    import org.eclipse.emf.common.util.EList;
    import org.eclipse.emf.ecore.EAttribute;
    import org.eclipse.emf.ecore.EClass;
    import org.eclipse.emf.ecore.EDataType;
    import org.eclipse.emf.ecore.EEnum;
    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.features.AbstractAlternativeFeature;
    import org.fortiss.variability.model.features.AbstractCompositionalFeature;
    import org.fortiss.variability.model.features.AbstractCrossFeatureConstraint;
    import org.fortiss.variability.model.features.AbstractFeature;
    import org.fortiss.variability.model.features.AbstractFeatureModel;
    import org.fortiss.variability.model.presence.AndPC;
    import org.fortiss.variability.model.presence.DefaultPC;
    import org.fortiss.variability.model.presence.ILiteralReferencable;
    import org.fortiss.variability.model.presence.LiteralPC;
    import org.fortiss.variability.model.presence.NotPC;
    import org.fortiss.variability.model.presence.OrPC;
    import org.fortiss.variability.model.presence.PresenceCondition;
    import org.fortiss.variability.model.presence.PresenceConditionTerm;
    import com.microsoft.z3.BoolExpr;
    import com.microsoft.z3.BoolSort;
    import com.microsoft.z3.Context;
    import com.microsoft.z3.EnumSort;
    import com.microsoft.z3.Expr;
    import com.microsoft.z3.FuncDecl;
    import com.microsoft.z3.IntSort;
    import com.microsoft.z3.SeqExpr;
    import com.microsoft.z3.SeqSort;
    import com.microsoft.z3.Solver;
    import com.microsoft.z3.Sort;
    import com.microsoft.z3.StringSymbol;
    import com.microsoft.z3.Symbol;
    /**
    * Base class that implements the translation of model product-lines to SMT in order to perform
    * product-line analysis via constraint lifting.
    *
    * @deprecated
    *
    * TODO: To be removed completely #4328 (https://git.fortiss.org/af3/af3/-/issues/4328)
    *
    * @author bayha
    */
    public class GenericProductLineTranslation implements IProductLineTranslation {
    /** Z3 sort for base type integer. */
    protected IntSort intSort;
    /** Z3 sort for base type string. */
    protected SeqSort stringSort;
    /** Z3 sort for base type boolean. */
    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>();
    /** 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>();
    /** Mapping of attributes to their translated Z3 function. */
    protected DualKeyMap<EAttribute, EClass, FuncDecl> eAttribute2FunDecl =
    new DualKeyMap<EAttribute, EClass, FuncDecl>();
    /** Mapping of references to their translated Z3 function. */
    protected DualKeyMap<EReference, EClass, FuncDecl> eReference2FunDecl =
    new DualKeyMap<EReference, EClass, FuncDecl>();
    /** Mapping of references to the respective translated Z3 type. */
    protected Map<EReference, Sort> eReference2Sort = new HashMap<EReference, Sort>();
    /** 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>();
    /** Mapping of class.reference to the respective z3 function. */
    protected DualKeyMap<EClass, String, FuncDecl> attRefNames2FuncDecl =
    new DualKeyMap<EClass, String, FuncDecl>();
    /**
    * 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 =
    new DualKeyMap<EObject, EClass, Expr>();
    protected Map<Expr, EObject> expr2EObject = new HashMap<Expr, EObject>();
    /** Mapping of enumeration literals to the translated Z3 expression. */
    protected Map<Enum<?>, Expr> eLiteral2Expr = new HashMap<Enum<?>, Expr>();
    /** Mapping of classes to their respective z3 expression for 'null' */
    protected Map<EClass, Expr> eClass2NullElement = new HashMap<EClass, Expr>();
    /** Mapping of enumerations to their respective z3 expression for 'null' */
    protected Map<EEnum, Expr> eEnum2NullElement = new HashMap<EEnum, Expr>();
    /** Mapping of feature names to corresponding Z3 Expr. */
    protected Map<String, BoolExpr> featureName2BoolExpr = new HashMap<String, BoolExpr>();
    /** Mapping of classes to the selection function (lambda) for this type. */
    protected Map<EClass, FuncDecl> eClass2SelectionFunction = new HashMap<EClass, FuncDecl>();
    /** Mapping of objects to their presence conditions. */
    protected Map<EObject, BoolExpr> eObject2Selection = new HashMap<EObject, BoolExpr>();
    /** {@link Context} to capture the translated model. */
    protected Context ctx = new Context();
    /** List of all translated assertions for the model. */
    protected List<BoolExpr> modelAssertions = new ArrayList<BoolExpr>();
    /** List of all assertions for the feature model. */
    protected List<BoolExpr> featureModelAssertions = new ArrayList<BoolExpr>();
    /** List of all assertions which encode the presence conditions. */
    protected List<BoolExpr> presenceConditionAssertions = new ArrayList<BoolExpr>();
    protected List<BoolExpr> constraintAssertions = new ArrayList<BoolExpr>();
    /**
    * Constructor.
    */
    protected GenericProductLineTranslation() {
    initialize();
    }
    /** Returns the mapping from {@link EClass} to Z3 {@link EnumSort}. */
    public Map<EClass, EnumSort> geteClass2Datatype() {
    return eClass2Datatype;
    }
    /** Returns attRefNames2FuncDecl. */
    public DualKeyMap<EClass, String, FuncDecl> getAttRefNames2FuncDecl() {
    return attRefNames2FuncDecl;
    }
    /** Returns boolSort. */
    public BoolSort getBoolSort() {
    return boolSort;
    }
    /** Returns expr2EObject. */
    public Map<Expr, EObject> getExpr2EObject() {
    return expr2EObject;
    }
    /**
    * Initialization of analysis and base types.
    */
    private void initialize() {
    intSort = ctx.mkIntSort();
    stringSort = ctx.mkStringSort();
    boolSort = ctx.mkBoolSort();
    eDataType2Sort.put(EcorePackage.Literals.EINT, intSort);
    eDataType2Sort.put(EcorePackage.Literals.ESTRING, stringSort);
    eDataType2Sort.put(EcorePackage.Literals.EBOOLEAN, boolSort);
    }
    /** 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);
    }
    }
    /** Performs the complete translation of the product-line to Z3. */
    public void translateModel(EObject model) {
    // Prepare the core translation
    excludeClassesAndReferences();
    translateFeatureModel(model);
    collectClassesAndObjectsRecrsively(model);
    // Metamodel translation
    translateClassesMetamodel();
    translateAttributesAndReferencesMetamodel();
    // Translate variability
    translatePresenceConditions();
    // Model translation
    translateObjects();
    }
    /** Translates the presence conditions to Z3. */
    protected void translatePresenceConditions() {
    for(EClass ec : allObjects.keySet()) {
    EnumSort ecSort = eClass2Datatype.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);
    // If there is no PC term yet, create one
    if(eoSelection == null) {
    final PresenceConditionTerm globalPC = getGlobalPresenceConditionForEObject(eo);
    eoSelection = translatePresenceCondition(globalPC);
    if(eoSelection == null) {
    eoSelection = ctx.mkTrue();
    }
    eObject2Selection.put(eo, eoSelection);
    }
    Expr eoExpr = eObject2Expr.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);
    }
    /** Translates a given {@link PresenceCondition} to Z3. */
    private BoolExpr translatePresenceCondition(PresenceCondition pc) {
    if(pc == null) {
    return null;
    }
    if(pc instanceof LiteralPC) {
    ILiteralReferencable literal = ((LiteralPC)pc).getLiteralReference();
    if(literal == null || literal.getName().length() == 0) {
    // Illegal literals are translated as true.
    return ctx.mkTrue();
    }
    return featureName2BoolExpr.get(literal.getName());
    }
    if(pc instanceof DefaultPC) {
    return translatePresenceCondition(pc.resolveToFeatureLiterals());
    }
    if(pc instanceof OrPC) {
    PresenceConditionTerm op1 = ((OrPC)pc).getOperand1();
    PresenceConditionTerm op2 = ((OrPC)pc).getOperand2();
    return ctx.mkOr(translatePresenceCondition(op1), translatePresenceCondition(op2));
    }
    if(pc instanceof AndPC) {
    PresenceConditionTerm op1 = ((AndPC)pc).getOperand1();
    PresenceConditionTerm op2 = ((AndPC)pc).getOperand2();
    return ctx.mkAnd(translatePresenceCondition(op1), translatePresenceCondition(op2));
    }
    if(pc instanceof NotPC) {
    return ctx.mkNot(translatePresenceCondition(((NotPC)pc).getOperand()));
    }
    logError("Unknown PresenceCondition: " + pc);
    return null;
    }
    /** 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) {
    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);
    featureModelAssertions.add(fmExpr);
    // Translate all features (including alternatives)
    for(AbstractFeature f : getChildrenWithType(fm, AbstractFeature.class)) {
    String name = f.getName();
    String constName = "FEATURE_" + name;
    final BoolExpr fExpr = ctx.mkBoolConst(constName.replaceAll("@", "AT"));
    featureName2BoolExpr.put(name, fExpr);
    // If f is child of another feature, the selection criteria have to be encoded.
    final EObject fContainer = f.eContainer();
    if(fContainer instanceof AbstractFeature) {
    AbstractFeature parentF = (AbstractFeature)fContainer;
    final BoolExpr parentExpr = featureName2BoolExpr.get(parentF.getName());
    if(f.isOptional()) {
    featureModelAssertions.add(ctx.mkImplies(fExpr, parentExpr));
    } else {
    if(fContainer instanceof AbstractCompositionalFeature) {
    featureModelAssertions.add(ctx.mkImplies(parentExpr, fExpr));
    }
    }
    }
    }
    // For alternatives also translate the alternative selection criteria
    for(AbstractAlternativeFeature af : getChildrenWithType(fm,
    AbstractAlternativeFeature.class)) {
    BoolExpr afExpr = featureName2BoolExpr.get(af.getName());
    EList<AbstractFeature> as = af.getAlternatives();
    featureModelAssertions.add(ctx.mkImplies(afExpr,
    ctx.mkOr(as.stream().map(alt -> featureName2BoolExpr.get(alt.getName()))
    .collect(toList()).toArray(new BoolExpr[0]))));
    for(AbstractFeature a : as) {
    BoolExpr aExpr = featureName2BoolExpr.get(a.getName());
    featureModelAssertions.add(ctx.mkImplies(aExpr, afExpr));
    featureModelAssertions.add(ctx.mkImplies(aExpr,
    ctx.mkAnd(as.stream().filter(alt -> alt != a)
    .map(alt -> ctx.mkNot(featureName2BoolExpr.get(alt.getName())))
    .collect(toList()).toArray(new BoolExpr[0]))));
    }
    }
    // Translate all constraints.
    for(AbstractCrossFeatureConstraint c : getChildrenWithType(fm,
    AbstractCrossFeatureConstraint.class)) {
    AbstractFeature target = c.getTarget();
    AbstractFeature source = (AbstractFeature)c.eContainer();
    BoolExpr srcExpr = featureName2BoolExpr.get(source.getName());
    BoolExpr trgExpr = featureName2BoolExpr.get(target.getName());
    switch(c.getType()) {
    case REQUIRES:
    featureModelAssertions.add(ctx.mkImplies(srcExpr, trgExpr));
    break;
    case EXCLUDES:
    featureModelAssertions.add(ctx.mkImplies(srcExpr, ctx.mkNot(trgExpr)));
    break;
    default: // Suggestions are not translated.
    }
    }
    }
    /** Mapping from tracking variables to z3 expression (used for counterexample extraction). */
    // protected Map<BoolExpr, BoolExpr> tracToExpr = new HashMap<BoolExpr, BoolExpr>();
    /** Creates and initializes the Z3 solver to be used for analyis. */
    public Solver createSolver() {
    Solver solver = ctx.mkSolver();// ctx.mkTactic("psmt"));
    solver.add(featureModelAssertions.toArray(new BoolExpr[featureModelAssertions.size()]));
    solver.add(presenceConditionAssertions
    .toArray(new BoolExpr[presenceConditionAssertions.size()]));
    solver.add(modelAssertions.toArray(new BoolExpr[modelAssertions.size()]));
    solver.add(constraintAssertions.toArray(new BoolExpr[constraintAssertions.size()]));
    //
    // List<BoolExpr> tracFeaturesList = featureModelAssertions.stream()
    // .map(a -> ctx.mkBoolConst("tracFeatureVar" + a.getId())).collect(toList());
    //
    // solver.assertAndTrack(
    // featureModelAssertions.toArray(new BoolExpr[featureModelAssertions.size()]),
    // tracFeaturesList.toArray(new BoolExpr[featureModelAssertions.size()]));
    // for(int i = 0; i < featureModelAssertions.size(); i++) {
    // tracToExpr.put(tracFeaturesList.get(i), featureModelAssertions.get(i));
    // }
    //
    // List<BoolExpr> tracPresenceList = presenceConditionAssertions.stream()
    // .map(a -> ctx.mkBoolConst("tracPresenceVar" + a.getId())).collect(toList());
    //
    // solver.assertAndTrack(
    // presenceConditionAssertions
    // .toArray(new BoolExpr[presenceConditionAssertions.size()]),
    // tracPresenceList.toArray(new BoolExpr[presenceConditionAssertions.size()]));
    //
    // for(int i = 0; i < presenceConditionAssertions.size(); i++) {
    // tracToExpr.put(tracPresenceList.get(i), presenceConditionAssertions.get(i));
    // }
    // BoolExpr[] assertionsArray = modelAssertions.toArray(new
    // BoolExpr[modelAssertions.size()]);
    // List<BoolExpr> tracList = modelAssertions.stream()
    // .map(a -> ctx.mkBoolConst("tracModelVar" + a.getId())).collect(toList());
    // BoolExpr[] assertionsTracArray = tracList.toArray(new BoolExpr[modelAssertions.size()]);
    //
    // for(int i = 0; i < modelAssertions.size(); i++) {
    // tracToExpr.put(tracList.get(i), modelAssertions.get(i));
    // }
    //
    // solver.assertAndTrack(assertionsArray, assertionsTracArray);
    return solver;
    }
    /** Translates all objects in the model. */
    private void translateObjects() {
    // Translate objects by class.
    for(EClass ec : allObjects.keySet()) {
    Set<EObject> Objs = allObjects.get(ec);
    Set<EAttribute> attributes = translatedAttributes.get(ec);
    if(attributes != null) {
    for(EAttribute ea : attributes) {
    FuncDecl attFunc = eAttribute2FunDecl.get(ea, ec);
    for(EObject eo : Objs) {
    Expr attVal = translateAttributeValue(eo, ea);
    BoolExpr attValAssertion =
    ctx.mkEq(ctx.mkApp(attFunc, eObject2Expr.get(eo, ec)), attVal);
    modelAssertions.add(attValAssertion);
    }
    }
    }
    Set<EReference> references = translatedReferences.get(ec);
    if(references != null) {
    for(EReference er : references) {
    FuncDecl refFunc = eReference2FunDecl.get(er, ec);
    for(EObject eo : Objs) {
    Expr eoExpr = eObject2Expr.get(eo, ec);
    Expr refVal = translateReferenceValue(eo, er);
    BoolExpr rafValAssertion = ctx.mkEq(ctx.mkApp(refFunc, eoExpr), refVal);
    modelAssertions.add(rafValAssertion);
    }
    // Null must always only point to null....
    EClass refType = er.getEReferenceType();
    Expr nullElement = eClass2NullElement.get(ec);
    if(er.getUpperBound() > 0) {
    modelAssertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
    eClass2NullElement.get(refType)));
    } else {
    modelAssertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
    ctx.mkEmptySeq(eReference2Sort.get(er))));
    }
    }
    }
    }
    }
    /** Translates the given instance of a relation between individual objects in the model. */
    private Expr translateReferenceValue(EObject eo, EReference er) {
    Object value = eo.eGet(er);
    EClass refType = er.getEReferenceType();
    Expr refNullValue = eClass2NullElement.get(refType);
    FuncDecl refSelFun = eClass2SelectionFunction.get(er.getEType());
    if(er.getUpperBound() < 0) {
    // Case for lists
    List<?> values = (List<?>)value;
    if(values.size() == 0) {
    return ctx.mkEmptySeq(eReference2Sort.get(er));
    }
    // 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);
    SeqExpr selectedExpr = ctx.mkUnit(elemExpr);
    if(refSelFun != null) {
    SeqExpr notSelectedExpr = ctx.mkEmptySeq(eReference2Sort.get(er));
    seqElems[i] = (SeqExpr)ctx.mkITE((BoolExpr)ctx.mkApp(refSelFun, elemExpr),
    selectedExpr, notSelectedExpr);
    } else {
    seqElems[i] = selectedExpr;
    }
    }
    if(seqElems.length == 0) {
    return ctx.mkEmptySeq(eReference2Sort.get(er));
    }
    if(seqElems.length == 1) {
    return seqElems[0];
    }
    return ctx.mkConcat(seqElems);
    }
    if(value == null) {
    return refNullValue;
    }
    Expr singleValExpr = eObject2Expr.get((EObject)value, refType);
    if(refSelFun != null) {
    // Case with variable target
    BoolExpr eoSel = (BoolExpr)ctx.mkApp(refSelFun, singleValExpr);
    return ctx.mkITE(eoSel, singleValExpr, refNullValue);
    }
    // Default case with non variable target.
    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));
    }
    /** Translates the given EAttribute value for the given object to Z3. */
    private Expr translateAttributeValue(EObject eo, EAttribute ea) {
    Object value = eo.eGet(ea);
    EDataType attType = ea.getEAttributeType();
    if(ea.getUpperBound() < 0 && value instanceof List<?>) {
    // Case for lists.
    List<?> values = (List<?>)value;
    SeqExpr[] seqElem = new SeqExpr[values.size()];
    for(int i = 0; i < values.size(); i++) {
    Object o = values.get(i);
    Expr elemExpr = traslatePrimitiveObject(o, attType);
    seqElem[i] = ctx.mkUnit(elemExpr);
    }
    return ctx.mkConcat(seqElem);
    }
    return traslatePrimitiveObject(value, attType);
    }
    /** Translates the given object for a primitive type (Enums, Integer, String, Boolean) to Z3. */
    private Expr traslatePrimitiveObject(Object value, EDataType attType) {
    // Single value
    if(attType.equals(EcorePackage.Literals.EINT)) {
    if(value == null) {
    logError("null int found");
    return ctx.mkInt(0);
    }
    return ctx.mkInt((int)value);
    }
    if(attType.equals(EcorePackage.Literals.ESTRING)) {
    if(value == null) {
    return ctx.mkString("");
    }
    return ctx.mkString((String)value);
    }
    if(attType.equals(EcorePackage.Literals.EBOOLEAN)) {
    if(value == null) {
    logError("null bool found");
    return ctx.mkBool(false);
    }
    return ctx.mkBool((boolean)value);
    }
    if(attType instanceof EEnum) {
    if(value == null) {
    return eEnum2NullElement.get(attType);
    }
    return eLiteral2Expr.get(value);
    }
    return null;
    }
    /** Creates functions for all attributes and references of the meta model in Z3. */
    private void translateAttributesAndReferencesMetamodel() {
    for(EClass ec : allObjects.keySet()) {
    for(EAttribute ea : ec.getEAllAttributes()) {
    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);
    }
    }
    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);
    eAttribute2FunDecl.put(ea, ec, funDecl);
    translatedAttributes.add(ec, ea);
    attRefNames2FuncDecl.put(ec, ea.getName(), funDecl);
    }
    for(EReference er : ec.getEAllReferences()) {
    String funId = ec.getName() + "_" + er.getName();
    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;
    }
    refSort = translateSuperType(refType);
    if(refSort == null) {
    // There are no instances of this type...
    continue;
    }
    }
    FuncDecl funDecl;
    if(er.getUpperBound() < 0) {
    // This is the case of unlimited multiplicity
    refSort = ctx.mkSeqSort(refSort);
    }
    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;
    }
    /** Translates the give enumeration */
    private Sort translateEnum(EEnum en) {
    String name = en.getName();
    EList<EEnumLiteral> enumLiterals = en.getELiterals();
    // Null needs to be encoded as a dedicated literal
    int numLiterals = enumLiterals.size();
    String[] literals = new String[numLiterals + 1];
    for(int i = 0; i < numLiterals; i++) {
    literals[i] = name + "_" + enumLiterals.get(i).getName();
    }
    literals[numLiterals] = name + "_NONE_LITERAL";
    EnumSort enumSort = ctx.mkEnumSort(name, literals);
    // Add regular literals and null literal to the respective mappings.
    for(int i = 0; i < numLiterals; i++) {
    eLiteral2Expr.put((Enum<?>)enumLiterals.get(i).getInstance(), enumSort.getConst(i));
    }
    eEnum2NullElement.put(en, enumSort.getConst(numLiterals));
    return enumSort;
    }
    /** 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));
    // The last index is added for the null element.
    Symbol[] objSymbols = new Symbol[objs.size() + 1];
    String clsName = cls.getName();
    for(int i = 0; i < objs.size(); i++) {
    String id = clsName + i;
    StringSymbol objSymbol = ctx.mkSymbol(id);
    objSymbols[i] = objSymbol;
    }
    objSymbols[objs.size()] = ctx.mkSymbol(clsName + "NONE");
    // Create EnumSort for class
    EnumSort enumSort = ctx.mkEnumSort(ctx.mkSymbol(clsName), objSymbols);
    eClass2Datatype.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]);
    expr2EObject.put(consts[i], objs.get(i));
    }
    Expr noneExpr = consts[consts.length - 1];
    eClass2NullElement.put(cls, noneExpr);
    }
    }
    /** Logs an error in the translation. */
    private void logError(String message) {
    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);
    }
    /** Returns ctx. */
    public Context getContext() {
    return ctx;
    }
    /** Returns eClass2NullElement. */
    public Map<EClass, Expr> getEClass2NullElement() {
    return eClass2NullElement;
    }
    /** {@inheritDoc} */
    @Override
    public EObject getEObjectForExpression(Expr<?> expr) {
    return expr2EObject.get(expr);
    }
    public FuncDecl<?> getSelectionFunction(EClass cls) {
    return eClass2SelectionFunction.get(cls);
    }
    /** {@inheritDoc} */
    @Override
    public Expr<?> getNullElement(EClass cls) {
    return eClass2NullElement.get(cls);
    }
    /** {@inheritDoc} */
    @Override
    public EnumSort getDatatype(EClass ec) {
    return eClass2Datatype.get(ec);
    }
    /** {@inheritDoc} */
    @Override
    public FuncDecl getAttributeReferenceFunctionDeclaration(EClass cVarType, String string) {
    return attRefNames2FuncDecl.get(cVarType, string);
    }
    /** {@inheritDoc} */
    @Override
    public void setTranslatedEClasses(Collection<EClass> clss) {
    // EMPTY
    }
    /** {@inheritDoc} */
    @Override
    public void setTranslatedEReferences(Collection<EReference> refs) {
    // EMPTY
    }
    /** {@inheritDoc} */
    @Override
    public void setTranslatedEAttributes(Collection<EAttribute> atts) {
    // EMPTY
    }
    /** {@inheritDoc} */
    @Override
    public Map<BoolExpr, IProductLineConstraint>
    translateConstraints(Collection<IProductLineConstraint> constraints) {
    Map<BoolExpr, IProductLineConstraint> constraintTracker2Constraint =
    new HashMap<BoolExpr, IProductLineConstraint>();
    for(IProductLineConstraint constraint : constraints) {
    Expr[] quantifierValiables = constraint.getQuantifierVariables();
    EClass[] variableClasses = constraint.getVariablesClasses();
    BoolExpr[] containmentExprs = new BoolExpr[0];
    BoolExpr body = constraint.getBody();
    boolean isForAll = constraint.isForAll();
    BoolExpr quantifier = createLiftedConstraint(quantifierValiables, variableClasses,
    containmentExprs, body, isForAll);
    BoolExpr constraintTracker =
    ctx.mkBoolConst("CONSTRAINT_" + constraint.getConstraintName());
    constraintTracker2Constraint.put(constraintTracker, constraint);
    constraintAssertions.add(ctx.mkEq(constraintTracker, quantifier));
    }
    Set<BoolExpr> allConstraints = constraintTracker2Constraint.keySet();
    constraintAssertions.add(ctx.mkOr(allConstraints.toArray(new BoolExpr[0])));
    return constraintTracker2Constraint;
    }
    /** Automatically lifts the given constraint */
    protected BoolExpr createLiftedConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
    BoolExpr[] containmentExprs, BoolExpr body, boolean isForAll) {
    BoolExpr[] selExprs = new BoolExpr[quantifierValiables.length + containmentExprs.length];
    for(int i = 0; i < quantifierValiables.length; i++) {
    EClass cls = variableClasses[i];
    Expr var = quantifierValiables[i];
    FuncDecl selFun = getSelectionFunction(cls);
    BoolExpr selected = (BoolExpr)ctx.mkApp(selFun, var);
    BoolExpr notNull = ctx.mkNot(ctx.mkEq(var, getNullElement(cls)));
    selExprs[i] = ctx.mkAnd(selected, notNull);
    }
    // Add containment expressions
    int j = 0;
    for(int i = quantifierValiables.length; i < quantifierValiables.length +
    containmentExprs.length; i++) {
    selExprs[i] = containmentExprs[j++];
    }
    if(isForAll) {
    BoolExpr liftedBody = ctx.mkImplies(ctx.mkAnd(selExprs), body);
    return ctx.mkForall(quantifierValiables, liftedBody, 0, null, null, null, null);
    }
    // else: Exits
    BoolExpr liftedBody = ctx.mkAnd(ctx.mkAnd(selExprs), body);
    return ctx.mkExists(quantifierValiables, liftedBody, 0, null, null, null, null);
    }
    }
    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