YELLOW

Issue-ref: 4240
Issue-URL: af3#4240

Signed-off-by: Andreas Bayha <bayha@fortiss.org>

org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings

-BucketMap.java c9572ca6503b41462240c1931cb1390af7b46c73 YELLOW
-BucketSetMap.java 2c87b2f7f9ac68ed0aa669d665a1f6cb91d27207 YELLOW
+BucketSetMap.java 407a35a6377ace1627c4c31890cfdc907f85945b YELLOW
 DualKeyMap.java 75fbe85a54e5a655aaf67108ae004f98ed2879d8 YELLOW
+IProductLineConstraint.java e9dfd0f5271420e9801b7728c718808e7316522e YELLOW
+ProductLineConstraintBase.java b112ea23bb618e8b5838943d3dede279f75b54b3 YELLOW
+ProductLineConstraintViolation.java a822cc970dc7bd08d6e702c123d86b4a6e05b9f0 YELLOW

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

-/*-------------------------------------------------------------------------+
-| 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.variability.analysis;
-
-import java.util.ArrayList;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
-
-/**
- * {@link Map} implementation which maps a key to a {@link List} of values.
- * 
- * @author bayha
- */
-public class BucketMap<K, V> extends HashMap<K, List<V>> {
-	/** ISerializable */
-	private static final long serialVersionUID = 312480465506162554L;
-
-	/**
-	 * Adds a given value to the list for the given key.
-	 * 
-	 * @param key
-	 *            The key for which an additional value shall be added.
-	 * @param value
-	 *            The additional value that shall be added.
-	 * 
-	 * @return The new list of values for the given key.
-	 */
-	public List<V> append(K key, V value) {
-		List<V> lst = this.get(key);
-
-		if(lst == null) {
-			lst = new ArrayList<V>();
-			this.put(key, lst);
-		}
-
-		lst.add(value);
-
-		return lst;
-	}
-}

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

@@ -39,16 +39,16 @@ public class BucketSetMap<K, V> extends HashMap<K, Set<V>> {
 	 * 
 	 * @return The new set of values for the given key.
 	 */
-	public Set<V> append(K key, V value) {
-		Set<V> lst = this.get(key);
+	public Set<V> add(K key, V value) {
+		Set<V> set = this.get(key);
 
-		if(lst == null) {
-			lst = new HashSet<V>();
-			this.put(key, lst);
+		if(set == null) {
+			set = new HashSet<V>();
+			this.put(key, set);
 		}
 
-		lst.add(value);
+		set.add(value);
 
-		return lst;
+		return set;
 	}
 }

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

@@ -25,26 +25,68 @@ import com.microsoft.z3.BoolExpr;
 import com.microsoft.z3.Expr;
 
 /**
+ * Interface for product line constraints to be checked by the {@link ProductLineBaseAnalysis}.
+ * 
+ * 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();
 
-	public String getConstraintMessage(List<EObject> violatingObjects,
+	/**
+	 * 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();
 
-	public EClass[] getVariablesClasses();
-
-	public BoolExpr[] getContainmentExpr();
-
+	/**
+	 * 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();
 
-	public List<Expr> getVariableTracker();
+	/**
+	 * 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();
 }

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.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;
+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 ProductLineBaseTranslation} to be used for creation of variables. */
+	protected ProductLineBaseTranslation translation;
+
+	/** Constructor. */
+	public ProductLineConstraintBase(ProductLineBaseTranslation translation) {
+		this.translation = translation;
+
+		variableTypes = createVariablesClasses();
+		variableNames = createVariableNames();
+		trackerVars = new Expr[variableNames.length];
+
+		createVariables();
+
+		body = createBody();
+
+		createTracking();
+	}
+
+	/** 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.geteClass2Datatype().get(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);
+		}
+	}
+
+	/** {@inheritDoc} */
+	@Override
+	public final Expr[] getQuantifierVariables() {
+		return variables;
+	}
+
+	/** Returns tracker. */
+	@Override
+	public final Expr[] getVariableTracker() {
+		return trackerVars;
+	}
+
+	/** Returns body. */
+	@Override
+	public final BoolExpr getBody() {
+		return body;
+	}
+
+	/** Returns variableTypes. */
+	@Override
+	public final EClass[] getVariablesClasses() {
+		return variableTypes;
+	}
+
+	/** 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 abstract boolean isForAll();
+
+	/** {@inheritDoc} */
+	@Override
+	public abstract String getConstraintName();
+
+	/** {@inheritDoc} */
+	@Override
+	public abstract String createErrorMessage(List<EObject> violatingObjects,
+			VariantConfiguration violatingConfiguration);
+}

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

@@ -21,22 +21,22 @@ 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 reuslt in a model variant which violates the constraint. */
 	private VariantConfiguration violatingConfiguration;
 
-	/**
-	 * @param constraint
-	 * @param violatingElements
-	 * @param violatingConfiguration
-	 */
+	/** Constructor. */
 	public ProductLineConstraintViolation(IProductLineConstraint constraint,
 			List<EObject> violatingElements, VariantConfiguration violatingConfiguration) {
 		this.constraint = constraint;
@@ -51,7 +51,7 @@ public class ProductLineConstraintViolation {
 
 	/** Returns errorMessage. */
 	public String getErrorMessage() {
-		return constraint.getConstraintMessage(violatingElements, violatingConfiguration);
+		return constraint.createErrorMessage(violatingElements, violatingConfiguration);
 	}
 
 	/** Returns constraint. */