From e80c550942b902c12dd629c90780ffa16c3a7bca Mon Sep 17 00:00:00 2001
From: Andreas Bayha <bayha@fortiss.org>
Date: Thu, 3 Aug 2023 11:33:40 +0200
Subject: [PATCH] YELLOW
Issue-ref: 4240
Issue-URL: https://git.fortiss.org/af3/af3/-/issues/4240
Signed-off-by: Andreas Bayha <bayha@fortiss.org>
---
.../org/fortiss/variability/analysis/.ratings | 8 +-
.../analysis/EMFProductLineTranslation.java | 320 +++++++++---------
.../analysis/IProductLineConstraint.java | 21 +-
.../analysis/IProductLineTranslation.java | 103 ++++--
.../analysis/ProductLineConstraintBase.java | 96 +++---
.../src/org/fortiss/variability/util/.ratings | 2 +-
.../util/VariabilityUtilsInternal.java | 69 +++-
7 files changed, 360 insertions(+), 259 deletions(-)
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings b/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings
index 87e0861f6..cab9866ef 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings
@@ -1,5 +1,7 @@
-BucketSetMap.java 407a35a6377ace1627c4c31890cfdc907f85945b YELLOW
+BucketSetMap.java 665a28c80a9693b9b9e31b7ebe59f2de4195d56c YELLOW
DualKeyMap.java 75fbe85a54e5a655aaf67108ae004f98ed2879d8 YELLOW
-IProductLineConstraint.java e9dfd0f5271420e9801b7728c718808e7316522e YELLOW
-ProductLineConstraintBase.java b112ea23bb618e8b5838943d3dede279f75b54b3 YELLOW
+EMFProductLineTranslation.java a9f4daf255db599cef1a0fe894f702d88b008cc0 YELLOW
+IProductLineConstraint.java 1b0e1231cc578a6e7e544441ac33533b4feafeb1 YELLOW
+IProductLineTranslation.java 733dae03e2baae237b6f0b33f0dd618a4f47cf73 YELLOW
+ProductLineConstraintBase.java 04097c7c31367fdd11a054ba2b259a0535a313f4 YELLOW
ProductLineConstraintViolation.java a822cc970dc7bd08d6e702c123d86b4a6e05b9f0 YELLOW
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
index 86aa2e7d2..a9f4daf25 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
@@ -5,6 +5,8 @@ import static org.eclipse.emf.ecore.util.EcoreUtil.copy;
import static org.fortiss.variability.model.VariabilityModelElementFactory.createAndPC;
import static org.fortiss.variability.util.VariabilityUtilsInternal.getAllReferences;
import static org.fortiss.variability.util.VariabilityUtilsInternal.getChildrenWithType;
+import static org.fortiss.variability.util.VariabilityUtilsInternal.logError;
+import static org.fortiss.variability.util.VariabilityUtilsInternal.logInfo;
import java.util.ArrayList;
import java.util.Collection;
@@ -63,94 +65,87 @@ import com.microsoft.z3.Symbol;
*/
public class EMFProductLineTranslation implements IProductLineTranslation {
- /*
- * FIXME: These should be
- * easier now, since we do not translate objects for all inheritance levels. Multiple
- * properties??.
- */
-
- /**
- * 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 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<?>> eObject2z3Expr =
- new DualKeyMap<EObject, EClass, Expr<?>>();
-
- /* Refactoring */
+ /** Prefix to be displayed as prefix to all logging messages from the translation. */
+ private static final String LOG_PREFIX = "[EMF product-line translation]: ";
/** {@link Context} to capture the translated model. */
- protected Context ctx;
+ private Context ctx;
/** Z3 sort for base type integer. */
- protected IntSort intSort;
+ private IntSort intSort;
/** Z3 sort for base type string. */
- protected SeqSort<?> stringSort;
+ private SeqSort<?> stringSort;
/** Z3 sort for base type boolean. */
- protected BoolSort boolSort;
+ private BoolSort boolSort;
/** List of all translated assertions for the model. */
- protected List<BoolExpr> modelAssertions;
+ private List<BoolExpr> modelAssertions;
/** List of all assertions for the feature model. */
- protected List<BoolExpr> featureModelAssertions;
+ private List<BoolExpr> featureModelAssertions;
/** List of all assertions which encode the presence conditions. */
- protected List<BoolExpr> presenceConditionAssertions;
+ private List<BoolExpr> presenceConditionAssertions;
/** List of all assertions which encode the constraints. */
- protected List<BoolExpr> constraintAssertions;
+ private List<BoolExpr> constraintAssertions;
/** Mapping of EDataTypes (e.g. EInt) to their translated Z3 type. */
- protected Map<EDataType, Sort> eDataType2Sort;
+ private Map<EDataType, Sort> eDataType2Sort;
/** Mapping for classes to their respective Z3 type. */
- protected Map<EClass, EnumSort<?>> eClass2z3Sort;
+ private Map<EClass, EnumSort<?>> eClass2z3Sort;
/** Mapping of enumeration literals to the translated Z3 expression. */
- protected Map<Enum<?>, Expr<?>> eLiteral2Expr;
+ private Map<Enum<?>, Expr<?>> eLiteral2Expr;
/** Mapping of classes to their respective z3 expression for 'null' */
- protected Map<EClass, Expr<?>> eClass2NullElement;
+ private Map<EClass, Expr<?>> eClass2NullElement;
/** Mapping of enumerations to their respective z3 expression for 'null' */
- protected Map<EEnum, Expr<?>> eEnum2NullElement;
+ private Map<EEnum, Expr<?>> eEnum2NullElement;
+
+ /** Mapping of attributes to their translated Z3 function. */
+ private DualKeyMap<EAttribute, EClass, FuncDecl<?>> eAttribute2FunDecl =
+ new DualKeyMap<EAttribute, EClass, FuncDecl<?>>();
+ /** Mapping of references to their translated Z3 function. */
+ private DualKeyMap<EReference, EClass, FuncDecl<?>> eReference2FunDecl =
+ new DualKeyMap<EReference, EClass, FuncDecl<?>>();
+
+ /**
+ * Mapping of objects with types to their translated Z3 expressions. The second key EClass is
+ * necessary as an object is translated for all classes specified in 'translatedClasses').
+ */
+ private DualKeyMap<EObject, EClass, Expr<?>> eObject2z3Expr =
+ new DualKeyMap<EObject, EClass, Expr<?>>();
/** Mapping of classes to the selection function for this type. */
- protected Map<EClass, FuncDecl<?>> eClass2SelectionFunction;
+ private Map<EClass, FuncDecl<?>> eClass2SelectionFunction;
/** The set to specify all {@link EClass} to be translated by this translation. */
- protected Set<EClass> translatedClasses;
+ private Set<EClass> translatedClasses;
/** The set to specify all {@link EReference} to be translated by this translation. */
- protected Set<EReference> translatedReferences;
+ private Set<EReference> translatedReferences;
/** The set to specify all {@link EAttribute} to be translated by this translation. */
- protected Set<EAttribute> translatedAttributes;
+ private Set<EAttribute> translatedAttributes;
/** The mapping of translated {@link EClass} to the objects that have been collected. */
- protected BucketSetMap<EClass, EObject> class2TranslatedEObjects;
+ private BucketSetMap<EClass, EObject> class2TranslatedEObjects;
/** The {@link AbstractFeatureModel} collected by this translation */
- protected AbstractFeatureModel featureModel;
+ private AbstractFeatureModel featureModel;
/** Mapping of features to corresponding Z3 {@link BoolExpr}. */
- protected Map<AbstractFeature, BoolExpr> feature2BoolExpr;
+ private Map<AbstractFeature, BoolExpr> feature2BoolExpr;
/** The mapping of translated {@link EObject}s to global {@link PresenceCondition}s. */
- protected Map<EObject, PresenceConditionTerm> object2presenceCondition;
+ private Map<EObject, PresenceConditionTerm> object2presenceCondition;
/**
* The mapping from Z3 {@link Expr} back to the respective {@link EObject} to be used for
* interpreting solver results.
*/
- protected Map<Expr<?>, EObject> expr2EObject = new HashMap<Expr<?>, EObject>();
+ private Map<Expr<?>, EObject> expr2EObject = new HashMap<Expr<?>, EObject>();
/**
* The mapping of translated {@link EReference}s to the type that will be used for translation.
* This type might be different from the references original type in case only a subtype is
* specified for translation.
*/
- protected Map<EReference, EClass> reference2TranslatedEClass;
+ private Map<EReference, EClass> reference2TranslatedEClass;
/** Flag that specifies whether the optimization to only translate optional parts is enabled. */
private boolean isIslandOptimizationEnabled = false;
@@ -246,16 +241,24 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
if(ecls.isSuperTypeOf(refType)) {
reference2TranslatedEClass.put(ref, ecls);
} else if(refType.isSuperTypeOf(ecls)) {
- // FIXME: Is this a good idea?
// Attempt to use nearest found class
reference2TranslatedEClass.put(ref, ecls);
+
+ logInfo(LOG_PREFIX + "The reference \"" + ref.getName() + "\" of type " +
+ refType.getName() +
+ " is supposed to be transletd for a prodct-line analysis. Since this type is not specified to be translated, the translated sub-class " +
+ ecls.getName() + " will be used.");
}
}
// Check if any super type was found
if(reference2TranslatedEClass.get(ref) == null) {
- throw new RuntimeException("ERefernce \"" + ref.getName() + "\" is of type " +
- ref.getEReferenceType().getName() + " which is not translated.");
+ String errMsg = LOG_PREFIX + "ERefernce \"" + ref.getName() + "\" is of type " +
+ ref.getEReferenceType().getName() + " which is not translated.";
+
+ logError(errMsg);
+
+ throw new RuntimeException(errMsg);
}
}
}
@@ -324,15 +327,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
for(EReference ref : model.eClass().getEAllReferences()) {
if(translatedReferences.contains(ref)) {
EObject refObj = (EObject)model.eGet(ref);
-
EClass refClass = reference2TranslatedEClass.get(ref);
- if(refClass != null) {
- class2TranslatedEObjects.add(refClass, refObj);
- } else {
- throw new RuntimeException("Invalid reference found. Reference " +
- ref.getName() + " is of type " + ref.getEReferenceType().getName() +
- " which is not translated.");
- }
+ class2TranslatedEObjects.add(refClass, refObj);
collectTranslatedReferences(refObj, remainingSteps - 1);
}
@@ -359,8 +355,6 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
class2TranslatedEObjects.add(cls, referencingEObject);
collectTranslatedReferences(referencingEObject, remainingSteps - 1);
-
- // break;
}
}
}
@@ -368,55 +362,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
}
- /**
- * Retrieves the {@link PresenceCondition} that was assigned to 'modelElement' in the model.
- * This function might be overwritten in case an alternative location for presence conditions
- * was defined.
- */
- protected PresenceConditionTerm getLocalPresenceCondition(EObject model) {
- if(model instanceof IOptionalVariationPoint<?>) {
- PresenceCondition presenceCondition =
- ((IOptionalVariationPoint<?>)model).getPresenceCondition();
-
- if(presenceCondition == null) {
- return null;
- }
-
- return presenceCondition.resolveToFeatureLiterals();
- }
- if(model instanceof IAlternative) {
- return ((IAlternative)model).getPresenceCondition().resolveToFeatureLiterals();
- }
-
- return null;
- }
-
- /** {@inheritDoc} */
- @Override
- public void setTranslatedEClasses(Collection<EClass> clss) {
- translatedClasses.clear();
-
- translatedClasses.addAll(clss);
- }
-
- /** {@inheritDoc} */
- @Override
- public void setTranslatedEReferences(Collection<EReference> refs) {
- translatedReferences.clear();
-
- translatedReferences.addAll(refs);
- }
-
- /** {@inheritDoc} */
- @Override
- public void setTranslatedEAttributes(Collection<EAttribute> atts) {
- translatedAttributes.clear();
-
- translatedAttributes.addAll(atts);
- }
-
/** Translates all presence conditions to Z3. */
- protected void translatePresenceConditions() {
+ private void translatePresenceConditions() {
for(EClass ec : translatedClasses) {
EnumSort<?> ecSort = eClass2z3Sort.get(ec);
FuncDecl<?> selFun = ctx.mkFuncDecl("SELECTED_" + ec.getName(), ecSort, boolSort);
@@ -473,7 +420,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
return ctx.mkNot(translatePresenceCondition(((NotPC)pc).getOperand()));
}
- logError("Unknown PresenceCondition: " + pc);
+ logError(LOG_PREFIX + "Unknown PresenceCondition: " + pc);
return null;
}
@@ -552,25 +499,10 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
}
- /** Creates and initializes the Z3 solver to be used for analyis. */
- @Override
- public Solver createSolver() {
- Solver solver = ctx.mkSolver();
-
- 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()]));
-
- return solver;
- }
-
/** Translates all objects in the model. */
private void translateObjects() {
// Translate objects by class.
- for(EClass ec : class2TranslatedEObjects.keySet()) {
+ for(EClass ec : translatedClasses) {
Set<EObject> objs = class2TranslatedEObjects.get(ec);
EList<EAttribute> attributes = ec.getEAllAttributes();
@@ -628,7 +560,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
List<?> values = (List<?>)value;
if(values.size() == 0) {
- return ctx.mkEmptySeq(eReferenceToz3Sort(er));
+ return ctx.mkEmptySeq(getSortForReference(er));
}
SeqExpr[] seqElems = new SeqExpr[values.size()];
@@ -639,7 +571,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
SeqExpr<?> selectedExpr = ctx.mkUnit(elemExpr);
if(refSelFun != null) {
- SeqExpr notSelectedExpr = ctx.mkEmptySeq(eReferenceToz3Sort(er));
+ SeqExpr notSelectedExpr = ctx.mkEmptySeq(getSortForReference(er));
seqElems[i] = (SeqExpr<?>)ctx.mkITE((BoolExpr)ctx.mkApp(refSelFun, elemExpr),
selectedExpr, notSelectedExpr);
} else {
@@ -648,7 +580,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
if(seqElems.length == 0) {
- return ctx.mkEmptySeq(eReferenceToz3Sort(er));
+ return ctx.mkEmptySeq(getSortForReference(er));
}
if(seqElems.length == 1) {
return seqElems[0];
@@ -702,7 +634,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
// Single value
if(attType.equals(EcorePackage.Literals.EINT)) {
if(value == null) {
- logError("null int found");
+ logError(LOG_PREFIX + "null int found");
return ctx.mkInt(0);
}
return ctx.mkInt((int)value);
@@ -715,7 +647,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
if(attType.equals(EcorePackage.Literals.EBOOLEAN)) {
if(value == null) {
- logError("null bool found");
+ logError(LOG_PREFIX + "null bool found");
return ctx.mkBool(false);
}
return ctx.mkBool((boolean)value);
@@ -768,18 +700,25 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
if(refSort == null) {
// Find translated subclass of reference target and attempt to use this.
- // TODO: Log message
for(EClass ecls : translatedClasses) {
if(refType.isSuperTypeOf(ecls)) {
refSort = eClass2z3Sort.get(ecls);
+
+ logInfo(LOG_PREFIX + "The reference \"" + er.getName() +
+ "\" of type " + refType.getName() +
+ " is supposed to be transletd for a prodct-line analysis. Since this type is not specified to be translated, the translated sub-class " +
+ ecls.getName() + " will be used.");
}
}
}
if(refSort == null) {
- throw new RuntimeException("Reference " + er.getName() +
+ String msg = "Reference " + er.getName() +
" shall be translated, but is of type " + refType.getName() +
- " which is not translated. Add the type to the translated classes to translate this reference.");
+ " which is not translated. Add the type to the translated classes to translate this reference.";
+
+ logError(LOG_PREFIX + msg, null);
+ throw new RuntimeException(msg);
}
if(er.getUpperBound() < 0) {
@@ -850,9 +789,19 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
}
- /** Logs an error in the translation. */
- private void logError(String message) {
- // FIXME //error(getDefault(), "Error in product-line translation: " + message);
+ /** {@inheritDoc} */
+ @Override
+ public Solver createSolver() {
+ Solver solver = ctx.mkSolver();
+
+ 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()]));
+
+ return solver;
}
/** {@inheritDoc} */
@@ -867,25 +816,12 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
return expr2EObject.get(expr);
}
- /** {@inheritDoc} FIXME: required?? */
- @Override
- public FuncDecl<?> getSelectionFunction(EClass cls) {
- return eClass2SelectionFunction.get(cls);
- }
-
/** {@inheritDoc} */
@Override
public Expr<?> getNullElement(EClass cls) {
return eClass2NullElement.get(cls);
}
- /** {@inheritDoc} */
- @Override
- @Deprecated
- public final void addExcludedClasses(Collection<EClass> excludedClasses) {
- // EMPTY
- }
-
/** {@inheritDoc} */
@Override
public EnumSort<?> getDatatype(EClass ec) {
@@ -951,7 +887,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
EClass cls = variableClasses[i];
Expr<?> var = quantifierValiables[i];
- FuncDecl<?> selFun = getSelectionFunction(cls);
+ FuncDecl<?> selFun = eClass2SelectionFunction.get(cls);
BoolExpr selected = (BoolExpr)ctx.mkApp(selFun, var);
BoolExpr notNull = ctx.mkNot(ctx.mkEq(var, getNullElement(cls)));
@@ -975,21 +911,87 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
return ctx.mkExists(quantifierValiables, liftedBody, 0, null, null, null, null);
}
- /** Sets isIslandOptimizationEnabled. TODO */
- public void setIslandOptimizationEnabled(boolean isIslandOptimizationEnabled) {
- this.isIslandOptimizationEnabled = isIslandOptimizationEnabled;
+ /** Utility method to get the z3 sort for a given reference. */
+ private EnumSort<?> getSortForReference(EReference er) {
+ return eClass2z3Sort.get(reference2TranslatedEClass.get(er));
}
- /** Sets islandOptimizationStepNum. TODO */
- public void setIslandOptimizationStepNum(int islandOptimizationStepNum) {
- this.islandOptimizationStepNum = islandOptimizationStepNum;
+ /**
+ * Retrieves the {@link PresenceCondition} that was assigned to 'modelElement' in the model.
+ * This function might be overwritten in case an alternative location for presence conditions
+ * was defined.
+ */
+ protected PresenceConditionTerm getLocalPresenceCondition(EObject model) {
+ if(model instanceof IOptionalVariationPoint<?>) {
+ PresenceCondition presenceCondition =
+ ((IOptionalVariationPoint<?>)model).getPresenceCondition();
+
+ if(presenceCondition == null) {
+ return null;
+ }
+
+ return presenceCondition.resolveToFeatureLiterals();
+ }
+ if(model instanceof IAlternative) {
+ return ((IAlternative)model).getPresenceCondition().resolveToFeatureLiterals();
+ }
+
+ return null;
+ }
+
+ /** {@inheritDoc} */
+ @Override
+ public void setTranslatedEClasses(Collection<EClass> clss) {
+ translatedClasses.clear();
+
+ translatedClasses.addAll(clss);
+ }
+
+ /** {@inheritDoc} */
+ @Override
+ public void setTranslatedEReferences(Collection<EReference> refs) {
+ translatedReferences.clear();
+
+ translatedReferences.addAll(refs);
+ }
+
+ /** {@inheritDoc} */
+ @Override
+ public void setTranslatedEAttributes(Collection<EAttribute> atts) {
+ translatedAttributes.clear();
+
+ translatedAttributes.addAll(atts);
}
/**
- * @param er
- * @return
+ * Enables or disables the "island optimization" for which only optional parts of the model are
+ * translated.
+ * This optimization is disbaled by default.
+ *
+ * Via the method {@code setIslandOptimizationStepNum()} it is possible to specify a range of
+ * transitive references to be guaranteed to be translated for all optional elements.
+ * Note, that this step size might be crucial for a constraint to checked correctly for
+ * interactions between optional and non-optional elements.
+ *
+ * @param setEnabled
+ * 'true' will enable the island optimization; 'false' will disbale.
*/
- private EnumSort<?> eReferenceToz3Sort(EReference er) {
- return eClass2z3Sort.get(reference2TranslatedEClass.get(er));
+ public void setIslandOptimizationEnabled(boolean setEnabled) {
+ this.isIslandOptimizationEnabled = setEnabled;
+ }
+
+ /**
+ * Specifies a number of transitive references starting from every optional element that will be
+ * guaranteed to be translated - even if they are non-optional.
+ *
+ * Note, that this step size might be crucial for a constraint to checked correctly for
+ * interactions between optional and non-optional elements.
+ *
+ * @param stepNum
+ * The number of trabnsitive references to be guaranteed to be translated for all
+ * optional elements.
+ */
+ public void setIslandOptimizationStepNum(int stepNum) {
+ this.islandOptimizationStepNum = stepNum;
}
}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java
index 7ddf34012..1b0e1231c 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java
@@ -62,7 +62,7 @@ public interface IProductLineConstraint {
*
* @return An array of variables as {@link Expr}s.
*/
- public Expr[] getQuantifierVariables();
+ public Expr<?>[] getQuantifierVariables();
/**
* Retrieves the constrain body for this constraint.
@@ -84,7 +84,7 @@ public interface IProductLineConstraint {
*
* @return An array of {@link Expr}s with the quantifier variables.
*/
- public Expr[] getVariableTracker();
+ public Expr<?>[] getVariableTracker();
/**
* Retrieves the {@link EClass} types for the quantified variables.
@@ -93,9 +93,26 @@ public interface IProductLineConstraint {
*/
public EClass[] getVariablesClasses();
+ /**
+ * Specifies the classes which need to be translated in order to evaluate this constraint.
+ *
+ * @return A {@link Collection} with all {@link EClass} which will be required to be translated.
+ */
public Collection<EClass> getTranslatedClasses();
+ /**
+ * Specifies the references which are used in this constraint and need to translated.
+ *
+ * @return A {@link Collection} with all {@link EReference} which will be required to be
+ * translated.
+ */
public Collection<EReference> getTranslatedReferences();
+ /**
+ * Specifies the attributes which are used in this constraint and need to translated.
+ *
+ * @return A {@link Collection} with all {@link EAttribute} which will be required to be
+ * translated.
+ */
public Collection<EAttribute> getTranslatedAttributes();
}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineTranslation.java
index 410a2dba4..733dae03e 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineTranslation.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineTranslation.java
@@ -31,74 +31,119 @@ import com.microsoft.z3.FuncDecl;
import com.microsoft.z3.Solver;
/**
+ * Interface for generic translation of model product-lines to SMT.
*
* @author bayha
*/
public interface IProductLineTranslation {
/**
- * @return
+ * Retrieves the context used for this translation.
+ *
+ * @return The Z3 {@link Context}.
*/
- Context getContext();
+ public Context getContext();
/**
+ * Translates the given model to Z3 SMT.
+ *
* @param model
+ * {@link EObject} with model to be translated.
*/
- void translateModel(EObject model);
+ public void translateModel(EObject model);
/**
+ * Translates the given product-line constraints to Z3 SMT.
+ *
* @param constraints
- * @return
+ * A {@link Collection} of {@link IProductLineConstraint} to be translated.
+ *
+ * @return A {@link Map} with Z3 {@link BoolExpr} to track the constraints in Z3
+ * models.
*/
- Map<BoolExpr, IProductLineConstraint>
+ public Map<BoolExpr, IProductLineConstraint>
translateConstraints(Collection<IProductLineConstraint> constraints);
/**
- * @return
+ * Retrieves the model element which was the source for the given Z3 expression.
+ *
+ * @param expr
+ * The Z3 {@link Expr} for which to retrieve the originating {@link EObject}.
+ *
+ * @return The {@link EObject} which was the source for the given Z3 expression.
*/
- EObject getEObjectForExpression(Expr<?> expr);
+ public EObject getEObjectForExpression(Expr<?> expr);
/**
- * @param tracToExpr
- * @return
+ * Creates and initializes the Z3 solver to be used for analyzes.
+ *
+ * Note, that {@code translateModel()} and {@code translateConstraints} should be called prior
+ * to this method.
+ *
+ * @return The Z3 {@link Solver} containing the model translation.
*/
- Solver createSolver();
+ public Solver createSolver();
/**
+ * Retrieves the Z3 expression representing null for the given {@link EClass}.
+ *
* @param cls
- * @return
+ * The {@link EClass} to retrieve the Z3 null element for.
+ * @return The Z3 {@link Expr} encoding null.
*/
- FuncDecl getSelectionFunction(EClass cls);
+ public Expr<?> getNullElement(EClass cls);
/**
- * @param cls
- * @return
+ * Retrieves the Z3 sort which represents the given EClass and its objects.
+ *
+ * @param eClass
+ * The {@link EClass} to get the Z3 sort for.
+ * @return The Z3 {@link EnumSort} for the given eClass.
*/
- Expr<?> getNullElement(EClass cls);
+ public EnumSort<?> getDatatype(EClass eClass);
/**
- * @param excludedClasses
+ * Retrieve the Z3 function declaration which represents the given attribute or reference for
+ * the given EClass.
+ *
+ * @param eClass
+ * The {@link EClass} for which to get a attribute or reference function.
+ * @param attRefName
+ * {@link String} with the name for the attribute or reference.
+ * @return A Z3 {@link FuncDecl} representing the attribute or reference.
*/
- @Deprecated
- void addExcludedClasses(Collection<EClass> excludedClasses);
+ FuncDecl<?> getAttributeReferenceFunctionDeclaration(EClass eClass, String attRefName);
/**
- * @param ec
- * @return
+ * Specifies the classes for which model elements shall be translated.
+ *
+ * Note, that all classes which are relevant for evaluating the constraints need to specified
+ * here, before staring a translation.
+ *
+ * @param clss
+ * A {@link Collection} of all {@link EClass} to be translated.
*/
- EnumSort getDatatype(EClass ec);
+ public void setTranslatedEClasses(Collection<EClass> clss);
/**
- * @param cVarType
- * @param string
- * @return
+ * Specifies the references which shall be translated.
+ *
+ * Note, that all references which are used in the constraints need to specified
+ * here, before staring a translation.
+ *
+ * @param refs
+ * A {@link Collection} of all {@link EReference} to be translated.
*/
- FuncDecl getAttributeReferenceFunctionDeclaration(EClass cVarType, String string);
-
- public void setTranslatedEClasses(Collection<EClass> clss);
-
public void setTranslatedEReferences(Collection<EReference> refs);
+ /**
+ * Specifies the attributes which shall be translated.
+ *
+ * Note, that all attributes which are used in the constraints need to specified
+ * here, before staring a translation.
+ *
+ * @param atts
+ * A {@link Collection} of all {@link EAttribute} to be translated.
+ */
public void setTranslatedEAttributes(Collection<EAttribute> atts);
-
}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintBase.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintBase.java
index 58afed3e0..04097c7c3 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintBase.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintBase.java
@@ -16,12 +16,9 @@
package org.fortiss.variability.analysis;
import java.util.HashMap;
-import java.util.List;
import java.util.Map;
import org.eclipse.emf.ecore.EClass;
-import org.eclipse.emf.ecore.EObject;
-import org.fortiss.variability.model.features.configuration.VariantConfiguration;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.EnumSort;
@@ -49,16 +46,16 @@ public abstract class ProductLineConstraintBase implements IProductLineConstrain
protected String[] variableNames;
/** The quantified variables */
- protected Expr[] variables;
+ protected Expr<?>[] variables;
/**
* The tracking constants which are used to extract violating interpretations for the quantifier
* variables.
*/
- protected Expr[] trackerVars;
+ protected Expr<?>[] trackerVars;
/** A map from variable names to expressions which can be used in the body. */
- protected Map<String, Expr> name2Variables = new HashMap<String, Expr>();
+ protected Map<String, Expr<?>> name2Variables = new HashMap<String, Expr<?>>();
/** The {@link IProductLineTranslation} to be used for creation of variables. */
protected IProductLineTranslation translation;
@@ -72,54 +69,31 @@ public abstract class ProductLineConstraintBase implements IProductLineConstrain
trackerVars = new Expr[variableNames.length];
}
- /** Creates tracking variables and adds them to the body. */
- private final void createTracking() {
- int numVariables = variableNames.length;
- BoolExpr[] trackExprs = new BoolExpr[numVariables + 1];
-
- for(int i = 0; i < variables.length; i++) {
- trackExprs[i] = translation.getContext().mkEq(trackerVars[i], variables[i]);
- }
-
- trackExprs[numVariables] = body;
-
- body = translation.getContext().mkAnd(trackExprs);
- }
-
- /** Creates the Z3 variables for this constraint, using the translation. */
- private final void createVariables() {
- int numVariables = variableTypes.length;
- variables = new Expr[numVariables];
-
- for(int i = 0; i < numVariables; i++) {
- EClass ec = variableTypes[i];
- EnumSort ecSort = translation.getDatatype(ec);
+ /** Creates the actual body for this constraint using the quantified variables. */
+ protected abstract BoolExpr createBody();
- String varName = variableNames[i];
- trackerVars[i] = translation.getContext().mkConst(TRACK_PREFIX + varName, ecSort);
+ /** Specifies the names for the quantified variables. */
+ protected abstract String[] createVariableNames();
- Expr var = translation.getContext().mkConst(varName, ecSort);
- variables[i] = var;
- name2Variables.put(varName, var);
- }
- }
+ /** Specifies the EClass types for the quantified variables. */
+ protected abstract EClass[] createVariablesClasses();
/** {@inheritDoc} */
@Override
- public final Expr[] getQuantifierVariables() {
+ public final Expr<?>[] getQuantifierVariables() {
if(variables == null) {
createVariables();
}
return variables;
}
- /** Returns tracker. */
+ /** {@inheritDoc} */
@Override
- public final Expr[] getVariableTracker() {
+ public final Expr<?>[] getVariableTracker() {
return trackerVars;
}
- /** Returns body. */
+ /** {@inheritDoc} */
@Override
public final BoolExpr getBody() {
if(variables == null) {
@@ -134,31 +108,41 @@ public abstract class ProductLineConstraintBase implements IProductLineConstrain
return body;
}
- /** Returns variableTypes. */
+ /** {@inheritDoc} */
@Override
public final EClass[] getVariablesClasses() {
return variableTypes;
}
- /** Creates the actual body for this constraint using the quantified variables. */
- protected abstract BoolExpr createBody();
+ /** Creates tracking variables and adds them to the body. */
+ private final void createTracking() {
+ int numVariables = variableNames.length;
+ BoolExpr[] trackExprs = new BoolExpr[numVariables + 1];
- /** Specifies the names for the quantified variables. */
- protected abstract String[] createVariableNames();
+ for(int i = 0; i < variables.length; i++) {
+ trackExprs[i] = translation.getContext().mkEq(trackerVars[i], variables[i]);
+ }
- /** Specifies the EClass types for the quantified variables. */
- protected abstract EClass[] createVariablesClasses();
+ trackExprs[numVariables] = body;
- /** {@inheritDoc} */
- @Override
- public abstract boolean isForAll();
+ body = translation.getContext().mkAnd(trackExprs);
+ }
- /** {@inheritDoc} */
- @Override
- public abstract String getConstraintName();
+ /** Creates the Z3 variables for this constraint, using the translation. */
+ private final void createVariables() {
+ int numVariables = variableTypes.length;
+ variables = new Expr[numVariables];
- /** {@inheritDoc} */
- @Override
- public abstract String createErrorMessage(List<EObject> violatingObjects,
- VariantConfiguration violatingConfiguration);
+ for(int i = 0; i < numVariables; i++) {
+ EClass ec = variableTypes[i];
+ EnumSort<?> ecSort = translation.getDatatype(ec);
+
+ String varName = variableNames[i];
+ trackerVars[i] = translation.getContext().mkConst(TRACK_PREFIX + varName, ecSort);
+
+ Expr<?> var = translation.getContext().mkConst(varName, ecSort);
+ variables[i] = var;
+ name2Variables.put(varName, var);
+ }
+ }
}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/util/.ratings b/org.fortiss.variability/src/org/fortiss/variability/util/.ratings
index 8f6b1c25d..253136c40 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/util/.ratings
+++ b/org.fortiss.variability/src/org/fortiss/variability/util/.ratings
@@ -1,4 +1,4 @@
FeatureModelTransformationUtils.java b38702296dcb48ff311b382bb9c05d2590e2dfac GREEN
Pair.java 2dfd7dc65f7b9ba09a120f1a6058d1e8e9556a37 GREEN
VariabilityUtils.java 3e57a37ced6396076c71227aea8de534381b6ace GREEN
-VariabilityUtilsInternal.java 3db6af80e349e41ef3e236e783feaf34ce773fd0 YELLOW
+VariabilityUtilsInternal.java c5a4c445e73a15826882361a75b5dca201c3ca91 YELLOW
diff --git a/org.fortiss.variability/src/org/fortiss/variability/util/VariabilityUtilsInternal.java b/org.fortiss.variability/src/org/fortiss/variability/util/VariabilityUtilsInternal.java
index 3db6af80e..c5a4c445e 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/util/VariabilityUtilsInternal.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/util/VariabilityUtilsInternal.java
@@ -16,9 +16,13 @@
+--------------------------------------------------------------------------*/
package org.fortiss.variability.util;
+import static org.eclipse.core.runtime.IStatus.ERROR;
+import static org.eclipse.core.runtime.IStatus.INFO;
+import static org.eclipse.core.runtime.IStatus.WARNING;
import static org.eclipse.emf.ecore.util.EcoreUtil.getAllContents;
import static org.eclipse.emf.ecore.util.EcoreUtil.getRootContainer;
import static org.eclipse.emf.ecore.util.EcoreUtil.UsageCrossReferencer.find;
+import static org.fortiss.variability.VariabilityActivator.getDefault;
import static org.fortiss.variability.model.VariabilityModelElementFactory.createAndPC;
import java.util.Collection;
@@ -26,9 +30,11 @@ import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Queue;
-import java.util.Set;
import java.util.function.Predicate;
+import org.eclipse.core.runtime.IStatus;
+import org.eclipse.core.runtime.Plugin;
+import org.eclipse.core.runtime.Status;
import org.eclipse.emf.common.util.BasicEList;
import org.eclipse.emf.common.util.EList;
import org.eclipse.emf.common.util.TreeIterator;
@@ -43,6 +49,9 @@ import org.fortiss.variability.model.presence.PresenceConditionTerm;
/**
* Utility functions that are used within the variability layers.
*
+ * This class contains duplicates of EcoreUtils of the fortiss Tooling Kernel to enable a usage of
+ * this variability plugin independent of the tooling kernel.
+ *
* @author bayha
*/
public class VariabilityUtilsInternal {
@@ -263,14 +272,56 @@ public class VariabilityUtilsInternal {
return rest;
}
- public static Class<? extends EObject> getContainedSuperClass(Class<?> subCls,
- Set<Class<? extends EObject>> clss) {
- for(Class<? extends EObject> t : clss) {
- if(t.isAssignableFrom(subCls)) {
- return t;
- }
- }
+ /**
+ * Logs a message that occurred in the context of the given plug-in with the
+ * given severity and a given {@link Throwable} that originally caused this
+ * log message.
+ */
+ private static void log(Plugin plugin, String message, int severity, Throwable cause) {
+ String pluginId = plugin.getBundle().getSymbolicName();
+ IStatus status = new Status(severity, pluginId, message, cause);
+ plugin.getLog().log(status);
+ }
+
+ /**
+ * Logs an info message that occurred in the context of the variability plug-in.
+ *
+ * @param message
+ * The {@link String} with the info message to be logged.
+ */
+ public static void logInfo(String message) {
+ log(getDefault(), message, INFO, null);
+ }
+
+ /**
+ * Logs a warning that occurred in the context of the variability plug-in.
+ *
+ * @param message
+ * The {@link String} with the warning message to be logged.
+ */
+ public static void logWarning(String message) {
+ log(getDefault(), message, WARNING, null);
+ }
+
+ /**
+ * Logs an error that occurred in the context of the variability plug-in.
+ *
+ * @param message
+ * The {@link String} with the error message to be logged.
+ * @param exception
+ * The {@link Exception} that originally caused this log message.
+ */
+ public static void logError(String message, Exception exception) {
+ log(getDefault(), message, ERROR, exception);
+ }
- return null;
+ /**
+ * Logs an error that occurred in the context of the variability plug-in.
+ *
+ * @param message
+ * The {@link String} with the error message to be logged.
+ */
+ public static void logError(String message) {
+ log(getDefault(), message, ERROR, null);
}
}
--
GitLab