Merge branch '4240' into 'master'

4240

Closes af3#4309 and af3#4240

See merge request !178

org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java

+/*-------------------------------------------------------------------------+
+| Copyright 2023 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.variability.analysis;
+
+import java.util.Collection;
+import java.util.List;
+
+import org.eclipse.emf.ecore.EAttribute;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.EReference;
+import org.fortiss.variability.model.features.configuration.VariantConfiguration;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Expr;
+
+/**
+ * Interface for product line constraints to be checked by the {@link GenericProductLineAnalysis}.
+ * 
+ * Note that usually this interface should not be implemented immediately. Instead use the base
+ * class {@link ProductLineConstraintBase} to define new constraints.
+ * 
+ * @author bayha
+ */
+public interface IProductLineConstraint {
+
+	/**
+	 * The name of the constraint.
+	 * 
+	 * @return The name as {@link String}.
+	 */
+	public String getConstraintName();
+
+	/**
+	 * Creates a meaningful error message for violations of this constraint.
+	 * 
+	 * @param violatingObjects
+	 *            The {@link EObject}s which violate the constraint in combination.
+	 * @param violatingConfiguration
+	 *            A {@link VariantConfiguration} which will result in a model variant in which the
+	 *            'violatingObjects' will violate this constraint.
+	 * @return The error message as a {@link String}.
+	 */
+	public String createErrorMessage(List<EObject> violatingObjects,
+			VariantConfiguration violatingConfiguration);
+
+	/**
+	 * Retrieves the quantified variables for this constraint.
+	 * 
+	 * @return An array of variables as {@link Expr}s.
+	 */
+	public Expr<?>[] getQuantifierVariables();
+
+	/**
+	 * Retrieves the constrain body for this constraint.
+	 * 
+	 * @return The constraint body as a {@link BoolExpr}.
+	 */
+	public BoolExpr getBody();
+
+	/**
+	 * Specifies whether this constraint is quantified as "for all".
+	 * 
+	 * @return 'true' if this constraint is quantified as "for all". 'false' if "exists".
+	 */
+	public boolean isForAll();
+
+	/**
+	 * Retrieves the generated tracker variables to identify violating interpretations for the
+	 * quantifier variables.
+	 * 
+	 * @return An array of {@link Expr}s with the quantifier variables.
+	 */
+	public Expr<?>[] getVariableTracker();
+
+	/**
+	 * Retrieves the {@link EClass} types for the quantified variables.
+	 * 
+	 * @return An array of {@link EClass}s for all quantified variables.
+	 */
+	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();
+}

org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineTranslation.java

+/*-------------------------------------------------------------------------+
+| Copyright 2023 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.variability.analysis;
+
+import java.util.Collection;
+import java.util.Map;
+
+import org.eclipse.emf.ecore.EAttribute;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.EReference;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.EnumSort;
+import com.microsoft.z3.Expr;
+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 {
+
+	/**
+	 * Retrieves the context used for this translation.
+	 * 
+	 * @return The Z3 {@link Context}.
+	 */
+	public Context getContext();
+
+	/**
+	 * Translates the given model to Z3 SMT.
+	 * 
+	 * @param model
+	 *            {@link EObject} with model to be translated.
+	 */
+	public void translateModel(EObject model);
+
+	/**
+	 * Translates the given product-line constraints to Z3 SMT.
+	 * 
+	 * @param constraints
+	 *            A {@link Collection} of {@link IProductLineConstraint} to be translated.
+	 * 
+	 * @return A {@link Map} with Z3 {@link BoolExpr} to track the constraints in Z3
+	 *         models.
+	 */
+	public Map<BoolExpr, IProductLineConstraint>
+			translateConstraints(Collection<IProductLineConstraint> constraints);
+
+	/**
+	 * 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.
+	 */
+	public EObject getEObjectForExpression(Expr<?> expr);
+
+	/**
+	 * 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.
+	 */
+	public Solver createSolver();
+
+	/**
+	 * Retrieves the Z3 expression representing null for the given {@link EClass}.
+	 * 
+	 * @param cls
+	 *            The {@link EClass} to retrieve the Z3 null element for.
+	 * @return The Z3 {@link Expr} encoding null.
+	 */
+	public Expr<?> getNullElement(EClass cls);
+
+	/**
+	 * 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.
+	 */
+	public EnumSort<?> getDatatype(EClass eClass);
+
+	/**
+	 * 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.
+	 */
+	FuncDecl<?> getAttributeReferenceFunctionDeclaration(EClass eClass, String attRefName);
+
+	/**
+	 * 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.
+	 */
+	public void setTranslatedEClasses(Collection<EClass> clss);
+
+	/**
+	 * 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.
+	 */
+	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);
+}

org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintBase.java

+/*-------------------------------------------------------------------------+
+| Copyright 2023 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.variability.analysis;
+
+import java.util.HashMap;
+import java.util.Map;
+
+import org.eclipse.emf.ecore.EClass;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.EnumSort;
+import com.microsoft.z3.Expr;
+
+/**
+ * Base class for product line constraints to be checked by the product-line analysis.
+ * 
+ * All constraints are quantified expressions of the form:
+ * [ForAll|Exists] <list of quantifed variables>: <body using quantified variables>
+ * 
+ * @author bayha
+ */
+public abstract class ProductLineConstraintBase implements IProductLineConstraint {
+	/** Prefix to label tracking variables. */
+	private static final String TRACK_PREFIX = "TRACK_";
+
+	/** The body of this constraint. I.e. the quantified expression. */
+	protected BoolExpr body;
+
+	/** The {@link EClass} types of the quantified variables. */
+	protected EClass[] variableTypes;
+
+	/** The names of the quantified variables. */
+	protected String[] variableNames;
+
+	/** The quantified variables */
+	protected Expr<?>[] variables;
+
+	/**
+	 * The tracking constants which are used to extract violating interpretations for the quantifier
+	 * variables.
+	 */
+	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<?>>();
+
+	/** The {@link IProductLineTranslation} to be used for creation of variables. */
+	protected IProductLineTranslation translation;
+
+	/** Constructor. */
+	public ProductLineConstraintBase(IProductLineTranslation translation) {
+		this.translation = translation;
+
+		variableTypes = createVariablesClasses();
+		variableNames = createVariableNames();
+		trackerVars = new Expr[variableNames.length];
+	}
+
+	/** Creates the actual body for this constraint using the quantified variables. */
+	protected abstract BoolExpr createBody();
+
+	/** Specifies the names for the quantified variables. */
+	protected abstract String[] createVariableNames();
+
+	/** Specifies the EClass types for the quantified variables. */
+	protected abstract EClass[] createVariablesClasses();
+
+	/** {@inheritDoc} */
+	@Override
+	public final Expr<?>[] getQuantifierVariables() {
+		if(variables == null) {
+			createVariables();
+		}
+		return variables;
+	}
+
+	/** {@inheritDoc} */
+	@Override
+	public final Expr<?>[] getVariableTracker() {
+		return trackerVars;
+	}
+
+	/** {@inheritDoc} */
+	@Override
+	public final BoolExpr getBody() {
+		if(variables == null) {
+			createVariables();
+		}
+
+		if(body == null) {
+			body = createBody();
+			createTracking();
+		}
+
+		return body;
+	}
+
+	/** {@inheritDoc} */
+	@Override
+	public final EClass[] getVariablesClasses() {
+		return variableTypes;
+	}
+
+	/** 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);
+
+			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);
+		}
+	}
+}

org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintViolation.java

+/*-------------------------------------------------------------------------+
+| Copyright 2023 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.variability.analysis;
+
+import java.util.List;
+
+import org.eclipse.emf.ecore.EObject;
+import org.fortiss.variability.model.features.configuration.VariantConfiguration;
+
+/**
+ * Class representing one error identified by a product line analysis run.
+ * 
+ * @author bayha
+ */
+public class ProductLineConstraintViolation {
+
+	/** The model elements which cause a constraint violation. */
+	protected List<EObject> violatingElements;
+
+	/** The violated constraint. */
+	protected IProductLineConstraint constraint;
+
+	/** The configuration which will result in a model variant which violates the constraint. */
+	private VariantConfiguration violatingConfiguration;
+
+	/** Constructor. */
+	public ProductLineConstraintViolation(IProductLineConstraint constraint,
+			List<EObject> violatingElements, VariantConfiguration violatingConfiguration) {
+		this.constraint = constraint;
+		this.violatingElements = violatingElements;
+		this.violatingConfiguration = violatingConfiguration;
+	}
+
+	/** 
+	 * Returns the elements which causes the violation. 
+	 * 
+	 * @return The elements which causes the violation.
+	 */
+	public List<EObject> getViolatingElements() {
+		return violatingElements;
+	}
+
+	/** 
+	 * Returns the error message. 
+	 * 
+	 * @return The error message. 
+	 */
+	public String getErrorMessage() {
+		return constraint.createErrorMessage(violatingElements, violatingConfiguration);
+	}
+
+	/** 
+	 * Returns the constraint that has been violated. 
+	 * 
+	 * @return The constraint that has been violated. 
+	 */
+	public IProductLineConstraint getConstraint() {
+		return constraint;
+	}
+
+	/** 
+	 * Returns the configuration which will violate the constraint. 
+	 * 
+	 * @return The configuration which will violate the constraint. 
+	 */
+	public VariantConfiguration getViolatingConfiguration() {
+		return violatingConfiguration;
+	}
+}

org.fortiss.variability/src/org/fortiss/variability/model/.ratings

 VariabilityModelElementFactory.java 5a50d78b0fc94a20329b95991b519a3e3fbf4410 GREEN
-VariabilityStaticImpl.java 96bc4364ebe635c94fafbd3ef60b8237b18c17c6 GREEN
+VariabilityStaticImpl.java 9d913de8c14b22b07d318084abd911c6d5692977 GREEN

org.fortiss.variability/src/org/fortiss/variability/model/VariabilityStaticImpl.java

@@ -17,10 +17,12 @@ package org.fortiss.variability.model;
 
 import static java.util.stream.Collectors.toList;
 import static org.eclipse.emf.ecore.util.EcoreUtil.delete;
+import static org.fortiss.tooling.kernel.utils.EcoreUtils.copy;
 import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
 import static org.fortiss.variability.model.VariabilityModelElementFactory.createAndPC;
 import static org.fortiss.variability.model.VariabilityModelElementFactory.createLiteralPC;
 import static org.fortiss.variability.model.VariabilityModelElementFactory.createNotPC;
+import static org.fortiss.variability.model.VariabilityModelElementFactory.createOrPC;
 
 import java.util.List;
 import java.util.stream.Stream;
@@ -335,4 +337,62 @@ public class VariabilityStaticImpl {
 		return target.getClass() == subject.getClass() &&
 				((AbstractFeature)target).getName().equals(subject.getName());
 	}
+
+	/**
+	 * Creates a new {@link PresenceConditionTerm} which is semantically equivalent to the given
+	 * {@link AndPC} but only uses features as literals.
+	 * 
+	 * @param and
+	 *            The {@link AndPC} to resolve.
+	 * @return A {@link PresenceConditionTerm} with features as literals, only.
+	 */
+	public static PresenceConditionTerm resolveToFeatureLiterals(AndPC and) {
+		return createAndPC(and.getOperand1().resolveToFeatureLiterals(),
+				and.getOperand2().resolveToFeatureLiterals(), "");
+	}
+
+	/**
+	 * Creates a new {@link PresenceConditionTerm} which is semantically equivalent to the given
+	 * {@link OrPC} but only uses features as literals.
+	 * 
+	 * @param or
+	 *            The {@link OrPC} to resolve.
+	 * @return A {@link PresenceConditionTerm} with features as literals, only.
+	 */
+	public static PresenceConditionTerm resolveToFeatureLiterals(OrPC or) {
+		return createOrPC(or.getOperand1().resolveToFeatureLiterals(),
+				or.getOperand2().resolveToFeatureLiterals(), "");
+	}
+
+	/**
+	 * Creates a new {@link PresenceConditionTerm} which is semantically equivalent to the given
+	 * {@link NotPC} but only uses features as literals.
+	 * 
+	 * @param not
+	 *            The {@link NotPC} to resolve.
+	 * @return A {@link PresenceConditionTerm} with features as literals, only.
+	 */
+	public static PresenceConditionTerm resolveToFeatureLiterals(NotPC not) {
+		return createNotPC(not.getOperand().resolveToFeatureLiterals(), "");
+	}
+
+	/**
+	 * Creates a new {@link PresenceConditionTerm} which is semantically equivalent to the given
+	 * {@link LiteralPC} but only uses features as literals.
+	 * 
+	 * In case the given literal refers to a feature already, the result will be syntactically
+	 * equivalent.
+	 * 
+	 * @param literal
+	 *            The {@link LiteralPC} to resolve.
+	 * @return A {@link PresenceConditionTerm} with features as literals, only.
+	 */
+	public static PresenceConditionTerm resolveToFeatureLiterals(LiteralPC literal) {
+		ILiteralReferencable reference = literal.getLiteralReference();
+		if(reference == null || reference instanceof AbstractFeature) {
+			return copy(literal);
+		}
+
+		return reference.resolveToFeatureLiterals();
+	}
 }

org.fortiss.variability/src/org/fortiss/variability/util/.ratings

 FeatureModelTransformationUtils.java b38702296dcb48ff311b382bb9c05d2590e2dfac GREEN
 Pair.java 2dfd7dc65f7b9ba09a120f1a6058d1e8e9556a37 GREEN
 VariabilityUtils.java 3e57a37ced6396076c71227aea8de534381b6ace GREEN
-VariabilityUtilsInternal.java 9c781a47513bb0c4ddcd13be1c27d62b70f25998 GREEN
+VariabilityUtilsInternal.java 612c248ae391aeeb0ad80a23abc50974004c5349 GREEN