From ea95f7925ac450e2a6b7148dcf5f98b991200a75 Mon Sep 17 00:00:00 2001
From: Andreas Bayha <bayha@fortiss.org>
Date: Tue, 25 Apr 2023 17:22:07 +0200
Subject: [PATCH] YELLOW
Issue-ref: 4240
Issue-URL: af3#4240
Signed-off-by: Andreas Bayha <bayha@fortiss.org>
---
.../org/fortiss/variability/analysis/.ratings | 6 +-
.../variability/analysis/BucketMap.java | 54 ------
.../variability/analysis/BucketSetMap.java | 14 +-
.../analysis/IProductLineConstraint.java | 54 +++++-
.../analysis/ProductLineConstraintBase.java | 158 ++++++++++++++++++
.../ProductLineConstraintViolation.java | 12 +-
6 files changed, 223 insertions(+), 75 deletions(-)
delete mode 100644 org.fortiss.variability/src/org/fortiss/variability/analysis/BucketMap.java
create mode 100644 org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintBase.java
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings b/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings
index a69031f1f..87e0861f6 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings
@@ -1,3 +1,5 @@
-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
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/BucketMap.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/BucketMap.java
deleted file mode 100644
index c9572ca65..000000000
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/BucketMap.java
+++ /dev/null
@@ -1,54 +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.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;
- }
-}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/BucketSetMap.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/BucketSetMap.java
index 2c87b2f7f..407a35a63 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/BucketSetMap.java
+++ b/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;
}
}
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 47d009b35..e9dfd0f52 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java
+++ b/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();
}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintBase.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintBase.java
new file mode 100644
index 000000000..b112ea23b
--- /dev/null
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintBase.java
@@ -0,0 +1,158 @@
+/*-------------------------------------------------------------------------+
+| 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);
+}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintViolation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintViolation.java
index 7d4de79b3..a822cc970 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintViolation.java
+++ b/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. */
--
GitLab