GREEN (+ small text fixes, etc.)

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



Signed-off-by: Sebastian Bergemann <bergemann@fortiss.org>

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

 BucketSetMap.java 665a28c80a9693b9b9e31b7ebe59f2de4195d56c GREEN
 DualKeyMap.java 75fbe85a54e5a655aaf67108ae004f98ed2879d8 GREEN
-EMFProductLineTranslation.java a62c588bd806fdf98d1e2fb4138c359528edcaad YELLOW
-GenericProductLineAnalysis.java 859b58aef54101734de849db293de79e16054098 GREEN
+EMFProductLineTranslation.java b590fbf053c21d9e6b0ee6d0818779e4adb1fe0b GREEN
+GenericProductLineAnalysis.java 1026cd6d7d0286c0f2402c5918d83cf7dc84407b GREEN
 GenericProductLineTranslation.java 2df1a1c1363cb93b6f498308e575833cf705e2fd GREEN
 IProductLineConstraint.java 1b0e1231cc578a6e7e544441ac33533b4feafeb1 GREEN
 IProductLineTranslation.java 733dae03e2baae237b6f0b33f0dd618a4f47cf73 GREEN

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

@@ -169,19 +169,15 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	/** Mapping of classes to the selection function for this type. */
 	private Map<EClass, FuncDecl<?>> eClass2SelectionFunction;
 
-	/**
-	 * Constructor.
-	 */
+	/** Constructor. */
 	public EMFProductLineTranslation() {
-		// Fields which should not change between individual translations are initialized only once
+		// Fields which should not change between individual translations are initialized only once.
 		translatedClasses = new HashSet<EClass>();
 		translatedReferences = new HashSet<EReference>();
 		translatedAttributes = new HashSet<EAttribute>();
 	}
 
-	/**
-	 * Initialization of analysis and base types.
-	 */
+	/** Initialization of analysis and base types. */
 	private void initialize() {
 		ctx = new Context();
 
@@ -205,6 +201,9 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		z3Expr2EObject = new HashMap<Expr<?>, EObject>();
 
 		eObject2referencingEObjects = new HashMap<EObject, BucketSetMap<EReference, EObject>>() {
+			/** ISerializable */
+			private static final long serialVersionUID = -4436109358184535028L;
+
 			/** {@inheritDoc} */
 			@Override
 			public BucketSetMap<EReference, EObject> get(Object key1) {
@@ -220,7 +219,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			}
 		};
 
-		// Initialize model independent base types
+		// Initialize model independent base types.
 		intSort = ctx.mkIntSort();
 		stringSort = ctx.mkStringSort();
 		boolSort = ctx.mkBoolSort();
@@ -233,10 +232,10 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	/** {@inheritDoc} */
 	@Override
 	public final void translateModel(EObject model) {
-		// Initialize and reset local fields
+		// Initialize and reset local fields.
 		initialize();
 
-		// Reference types need to be collected first, since they are required by optimizations in
+		// Reference types need to be collected first, since they are required by optimizations.
 		collectReferenceTypes();
 		collectTranslatedObjects(model, null);
 
@@ -244,14 +243,14 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			collectReferencedIslandObjects();
 		}
 
-		// Metamodel translation
+		// Metamodel translation.
 		translateClassesMetamodel();
 		translateAttributesAndReferencesMetamodel();
 
-		// Model translation
+		// Model translation.
 		translateObjects();
 
-		// Translate variability
+		// Translate variability.
 		translateFeatureModel();
 		translatePresenceConditions();
 	}
@@ -261,7 +260,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		for(EReference ref : translatedReferences) {
 			EClass refType = ref.getEReferenceType();
 
-			// Check if reference type is translated or is a subclass of a translated class
+			// Check if reference type is translated or is a subclass of a translated class.
 			EClass translatedRefType = getTranslatedClass(refType);
 			if(translatedRefType != null) {
 				reference2TranslatedEClass.put(ref, translatedRefType);
@@ -273,11 +272,11 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 
 						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 " +
+								" is supposed to be translated for a product-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
+				// Check if any super type was found.
 				if(reference2TranslatedEClass.get(ref) == null) {
 					String errMsg = LOG_PREFIX + "ERefernce \"" + ref.getName() + "\" is of type " +
 							ref.getEReferenceType().getName() + " which is not translated.";
@@ -320,7 +319,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			}
 		}
 
-		// For the island optimization all references (also non-variable) need to be collected
+		// For the island optimization, all references (also non-variable) need to be collected.
 		if(isIslandOptimizationEnabled) {
 			collectIncomingReferences(model);
 		}
@@ -369,7 +368,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			return;
 		}
 
-		// Collect outgoing references
+		// Collect outgoing references.
 		for(EReference ref : model.eClass().getEAllReferences()) {
 			if(translatedReferences.contains(ref)) {
 				EObject refObj = (EObject)model.eGet(ref);
@@ -380,7 +379,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			}
 		}
 
-		// Collect incoming references
+		// Collect incoming references.
 		BucketSetMap<EReference, EObject> incomingReferences =
 				eObject2referencingEObjects.get(model);
 		for(EReference ref : incomingReferences.keySet()) {
@@ -468,7 +467,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 
 		featureModelAssertions.add(fmExpr);
 
-		// Translate all features (including alternatives)
+		// Translate all features (including alternatives).
 		for(AbstractFeature f : getChildrenWithType(featureModel, AbstractFeature.class)) {
 			String name = f.getName();
 			String constName = "FEATURE_" + name;
@@ -491,7 +490,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			}
 		}
 
-		// For alternatives also translate the alternative selection criteria
+		// For alternatives also translate the alternative selection criteria.
 		for(AbstractAlternativeFeature af : getChildrenWithType(featureModel,
 				AbstractAlternativeFeature.class)) {
 			BoolExpr afExpr = feature2BoolExpr.get(af);
@@ -563,7 +562,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 						modelAssertions.add(rafValAssertion);
 					}
 
-					// Null must always only point to null....
+					// Null must always only point to null.
 					EClass refType = reference2TranslatedEClass.get(er);
 					Expr<?> nullElement = eClass2NullElement.get(ec);
 					if(er.getUpperBound() > 0) {
@@ -589,7 +588,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		FuncDecl<?> refSelFun = eClass2SelectionFunction.get(refType);
 
 		if(er.getUpperBound() < 0) {
-			// Case for lists
+			// Case for lists.
 			List<?> values = (List<?>)value;
 
 			if(values.size() == 0) {
@@ -628,7 +627,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		Expr singleValExpr = eObject2z3Expr.get((EObject)value, refType);
 
 		if(refSelFun != null) {
-			// Case with variable target
+			// Case with variable target.
 			BoolExpr eoSel = (BoolExpr)ctx.mkApp(refSelFun, singleValExpr);
 
 			return ctx.mkITE(eoSel, singleValExpr, refNullValue);
@@ -664,7 +663,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 
 	/** Translates the given object for a primitive type (Enums, Integer, String, Boolean) to Z3. */
 	private Expr<?> translatePrimitiveObject(Object value, EDataType attType) {
-		// Single value
+		// Single value.
 		if(attType.equals(EcorePackage.Literals.EINT)) {
 			if(value == null) {
 				logError(LOG_PREFIX + "null int found");
@@ -739,7 +738,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 
 								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 " +
+										" is supposed to be translated for a product-line analysis. Since this type is not specified to be translated, the translated sub-class " +
 										ecls.getName() + " will be used.");
 							}
 						}
@@ -755,7 +754,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 					}
 
 					if(er.getUpperBound() < 0) {
-						// This is the case of unlimited multiplicity, i.e. lists
+						// This is the case of unlimited multiplicity, i.e., lists.
 						refSort = ctx.mkSeqSort(refSort);
 					}
 
@@ -767,12 +766,12 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		}
 	}
 
-	/** Translates the give enumeration */
+	/** Translates the give enumeration. */
 	private Sort translateEnum(EEnum en) {
 		String name = en.getName();
 		EList<EEnumLiteral> enumLiterals = en.getELiterals();
 
-		// Null needs to be encoded as a dedicated literal
+		// Null needs to be encoded as a dedicated literal.
 		int numLiterals = enumLiterals.size();
 		String[] literals = new String[numLiterals + 1];
 		for(int i = 0; i < numLiterals; i++) {
@@ -807,11 +806,11 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			}
 			objSymbols[objs.size()] = ctx.mkSymbol(clsName + "NONE");
 
-			// Create EnumSort for class
+			// Create EnumSort for class.
 			EnumSort<?> enumSort = ctx.mkEnumSort(ctx.mkSymbol(clsName), objSymbols);
 			eClass2z3Sort.put(cls, enumSort);
 
-			// Map objects to z3 enum literals
+			// Map objects to z3 enum literals.
 			Expr<?>[] consts = enumSort.getConsts();
 			for(int i = 0; i < objs.size(); i++) {
 				eObject2z3Expr.put(objs.get(i), cls, consts[i]);
@@ -831,7 +830,6 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		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;
@@ -910,7 +908,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		return constraintTracker2Constraint;
 	}
 
-	/** Automatically lifts the given constraint */
+	/** Automatically lifts the given constraint. */
 	protected BoolExpr createLiftedConstraint(Expr<?>[] quantifierValiables,
 			EClass[] variableClasses, BoolExpr[] containmentExprs, BoolExpr body,
 			boolean isForAll) {
@@ -927,7 +925,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			selExprs[i] = ctx.mkAnd(selected, notNull);
 		}
 
-		// Add containment expressions
+		// Add containment expressions.
 		int j = 0;
 		for(int i = quantifierValiables.length; i < quantifierValiables.length +
 				containmentExprs.length; i++) {
@@ -999,7 +997,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	/**
 	 * Enables or disables the "island optimization" for which only optional parts of the model are
 	 * translated.
-	 * This optimization is disbaled by default.
+	 * This optimization is disabled 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.
@@ -1007,7 +1005,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	 * interactions between optional and non-optional elements.
 	 * 
 	 * @param setEnabled
-	 *            'true' will enable the island optimization; 'false' will disbale.
+	 *            'true' will enable the island optimization; 'false' will disable.
 	 */
 	public void setIslandOptimizationEnabled(boolean setEnabled) {
 		this.isIslandOptimizationEnabled = setEnabled;
@@ -1021,7 +1019,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	 * interactions between optional and non-optional elements.
 	 * 
 	 * @param stepNum
-	 *            The number of trabnsitive references to be guaranteed to be translated for all
+	 *            The number of transitive references to be guaranteed to be translated for all
 	 *            optional elements.
 	 */
 	public void setIslandOptimizationStepNum(int stepNum) {

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

@@ -45,10 +45,8 @@ public abstract class GenericProductLineAnalysis {
 		this.translation = translation;
 	}
 
-	/**
-	 * Creates the {@link IProductLineConstraint}s to be checked by this analysis.
-	 */
-	protected abstract Collection<IProductLineConstraint> createConstriants();
+	/**  Creates the {@link IProductLineConstraint}s to be checked by this analysis. */
+	protected abstract Collection<IProductLineConstraint> createConstraints();
 
 	/**
 	 * Performs a product-line analysis for the given model.
@@ -57,7 +55,7 @@ public abstract class GenericProductLineAnalysis {
 	 *         analysis. 'false' otherwise.
 	 */
 	public List<ProductLineConstraintViolation> doCheck() {
-		plConstraints = createConstriants();
+		plConstraints = createConstraints();
 
 		setTranslatedMetamodelElements();