From c1bf57af99460236e53e85b5fdab50f24af85d48 Mon Sep 17 00:00:00 2001
From: Andreas Bayha <bayha@fortiss.org>
Date: Thu, 19 Oct 2023 10:09:47 +0200
Subject: [PATCH] Variability: Removed deprecated old PL-Analysis
Removed the old, deprecated product-line analysis which is no longer
used.
Issue-ref: 4328
Issue-URL: https://git.fortiss.org/af3/af3/-/issues/4328
Signed-off-by: Andreas Bayha <bayha@fortiss.org>
---
.../tooling/ext/variability/analysis/.ratings | 2 -
.../analysis/ProductLineAnalysisBase.java | 96 --
.../analysis/ProductLineTranslationBase.java | 42 -
.../org/fortiss/variability/analysis/.ratings | 1 -
.../GenericProductLineTranslation.java | 949 ------------------
5 files changed, 1090 deletions(-)
delete mode 100644 org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineAnalysisBase.java
delete mode 100644 org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineTranslationBase.java
delete mode 100644 org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineTranslation.java
diff --git a/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/.ratings b/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/.ratings
index 38949ab25..db7c40539 100644
--- a/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/.ratings
+++ b/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/.ratings
@@ -1,4 +1,2 @@
OptimizedProductLineAnalysisBase.java 35a40c860cc8a9774a894600935c1ae89a5681a0 GREEN
OptimizedProductLineTranslation.java 415361dd35a04db219b06a1e40079452d7079b34 GREEN
-ProductLineAnalysisBase.java 891235573a2102279256585f8dc31934240b8dc1 GREEN
-ProductLineTranslationBase.java f24fb9343003c025bc4d2292d15bca543a548749 GREEN
diff --git a/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineAnalysisBase.java b/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineAnalysisBase.java
deleted file mode 100644
index 891235573..000000000
--- a/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineAnalysisBase.java
+++ /dev/null
@@ -1,96 +0,0 @@
-/*-------------------------------------------------------------------------+
-| 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);
- }
-}
diff --git a/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineTranslationBase.java b/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineTranslationBase.java
deleted file mode 100644
index f24fb9343..000000000
--- a/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineTranslationBase.java
+++ /dev/null
@@ -1,42 +0,0 @@
-/*-------------------------------------------------------------------------+
-| 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);
- }
-}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings b/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings
index 11afa1f97..5a84c1085 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings
@@ -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
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineTranslation.java
deleted file mode 100644
index 2df1a1c13..000000000
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineTranslation.java
+++ /dev/null
@@ -1,949 +0,0 @@
-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);
- }
-}
--
GitLab