Fixed parallel translation of multiple Objects

Objects which are referenced several times were also translated several
times. This has been fixed.

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
 DualKeyMap.java 75fbe85a54e5a655aaf67108ae004f98ed2879d8 YELLOW
-ProductLineTranslation.java 4ecd6805d3cd0b015ea013dcaf8a7bcc26f5b925 RED

org.fortiss.variability/src/org/fortiss/variability/analysis/BucketSetMap.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.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+
+/**
+ * {@link Map} implementation which maps a key to a {@link Set} of values.
+ * 
+ * @author bayha
+ */
+public class BucketSetMap<K, V> extends HashMap<K, Set<V>> {
+	/** ISerializable */
+	private static final long serialVersionUID = 312480465506162554L;
+
+	/**
+	 * Adds a given value to the set 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 set of values for the given key.
+	 */
+	public Set<V> append(K key, V value) {
+		Set<V> lst = this.get(key);
+
+		if(lst == null) {
+			lst = new HashSet<V>();
+			this.put(key, lst);
+		}
+
+		lst.add(value);
+
+		return lst;
+	}
+}

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

@@ -66,20 +66,20 @@ public class ProductLineBaseTranslation {
 	protected static BoolSort BOOL_SORT;
 
 	/** Mapping from classes to all their objects */
-	protected BucketMap<EClass, EObject> allObjects = new BucketMap<EClass, EObject>();
+	protected BucketSetMap<EClass, EObject> allObjects = new BucketSetMap<EClass, EObject>();
 	/** Mapping from classes to all their subclasses */
-	protected BucketMap<EClass, EClass> allSubclasses = new BucketMap<EClass, EClass>();
+	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 BucketMap<EClass, EAttribute> translatedAttributes =
-			new BucketMap<EClass, EAttribute>();
+	protected BucketSetMap<EClass, EAttribute> translatedAttributes =
+			new BucketSetMap<EClass, EAttribute>();
 	/** Mapping from classes to all references of the respective type. */
-	protected BucketMap<EClass, EReference> translatedReferences =
-			new BucketMap<EClass, EReference>();
+	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>();
@@ -380,9 +380,9 @@ public class ProductLineBaseTranslation {
 	private void translateObjects() {
 		// Translate objects by class.
 		for(EClass ec : allObjects.keySet()) {
-			List<EObject> Objs = allObjects.get(ec);
+			Set<EObject> Objs = allObjects.get(ec);
 
-			List<EAttribute> attributes = translatedAttributes.get(ec);
+			Set<EAttribute> attributes = translatedAttributes.get(ec);
 			if(attributes != null) {
 				for(EAttribute ea : attributes) {
 					FuncDecl attFunc = eAttribute2FunDecl.get(ea, ec);
@@ -396,7 +396,7 @@ public class ProductLineBaseTranslation {
 				}
 			}
 
-			List<EReference> references = translatedReferences.get(ec);
+			Set<EReference> references = translatedReferences.get(ec);
 			if(references != null) {
 				for(EReference er : references) {
 					FuncDecl refFunc = eReference2FunDecl.get(er, ec);
@@ -645,7 +645,7 @@ public class ProductLineBaseTranslation {
 	 * subtypes.
 	 */
 	private EnumSort translateSuperType(EClass refType) {
-		List<EClass> subClasses = allSubclasses.get(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;
@@ -702,9 +702,9 @@ public class ProductLineBaseTranslation {
 	/** Creates the types for all classes and objects in Z3. */
 	private void translateClassesMetamodel() {
 		for(EClass cls : allObjects.keySet()) {
-			List<EObject> objs = allObjects.get(cls);
+			List<EObject> objs = new ArrayList<EObject>(allObjects.get(cls));
 
-			// The last index is added for null.
+			// 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++) {
@@ -715,9 +715,11 @@ public class ProductLineBaseTranslation {
 			}
 			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]);