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

 BucketSetMap.java 665a28c80a9693b9b9e31b7ebe59f2de4195d56c YELLOW
 DualKeyMap.java 75fbe85a54e5a655aaf67108ae004f98ed2879d8 YELLOW
 EMFProductLineTranslation.java a9f4daf255db599cef1a0fe894f702d88b008cc0 YELLOW
+GenericProductLineAnalysis.java 6f6d48544ec2b872fa0a4f747a85657889ad463e YELLOW
 IProductLineConstraint.java 1b0e1231cc578a6e7e544441ac33533b4feafeb1 YELLOW
 IProductLineTranslation.java 733dae03e2baae237b6f0b33f0dd618a4f47cf73 YELLOW
 ProductLineConstraintBase.java 04097c7c31367fdd11a054ba2b259a0535a313f4 YELLOW

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

 package org.fortiss.variability.analysis;
 
-import static com.microsoft.z3.Status.UNSATISFIABLE;
+import static java.lang.System.currentTimeMillis;
+import static org.fortiss.variability.util.VariabilityUtilsInternal.logInfo;
 
-import java.io.FileNotFoundException;
-import java.io.PrintWriter;
 import java.util.ArrayList;
+import java.util.Collection;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
@@ -30,21 +30,28 @@ import com.microsoft.z3.Status;
  */
 public abstract class GenericProductLineAnalysis {
 
+	/** The product-line translation to be used. */
 	protected final IProductLineTranslation translation;
 
-	protected List<IProductLineConstraint> plConstraints = new ArrayList<IProductLineConstraint>();
-
+	/** {@link EObject} of the model to be translated. */
 	protected final EObject model;
 
+	/** The constraints to be checked by this analysis. */
+	protected Collection<IProductLineConstraint> plConstraints;
+
 	/**
 	 * Constructor.
 	 */
 	protected GenericProductLineAnalysis(EObject model, IProductLineTranslation translation) {
 		this.model = model;
-
 		this.translation = translation;
 	}
 
+	/**
+	 * Creates the {@link IProductLineConstraint}s to be checked by this analysis.
+	 */
+	protected abstract Collection<IProductLineConstraint> createConstriants();
+
 	/**
 	 * Performs a product-line analysis for the given model.
 	 * 
@@ -52,77 +59,37 @@ public abstract class GenericProductLineAnalysis {
 	 *         analysis. 'false' otherwise.
 	 */
 	public List<ProductLineConstraintViolation> doCheck() {
-		final long start = System.currentTimeMillis();
+		final long start = currentTimeMillis();
 
-		addConstriants();
+		plConstraints = createConstriants();
 
-		setTranslatedClassesAndReferences();
+		setTranslatedMetamodelElements();
 
 		translation.translateModel(model);
-
 		Map<BoolExpr, IProductLineConstraint> constraintTracker2Constraint =
 				translation.translateConstraints(plConstraints);
-
-		// addRawConstraints();
-
-		// Global.setParameter("parallel.enable", "true");
-
 		Solver solver = translation.createSolver();
 
 		String modelName = ((INamedElement)model).getName();
-		String path = "C:\\Users\\bayha\\tmp\\z3" + modelName + (start % 159739431) + "in";
-		try {
-			PrintWriter printWriter = new PrintWriter(path);
-			printWriter.println(solver);
-			printWriter.println("(check-sat)");
-			// printWriter.println("(get-model)");
-			printWriter.close();
-		} catch(FileNotFoundException e) {
-			// TODO Auto-generated catch block
-			e.printStackTrace();
-		}
 
-		long startSmt = System.currentTimeMillis();
+		final long startSmt = currentTimeMillis();
 
 		Status result = solver.check();
 
-		long end = System.currentTimeMillis();
+		final long end = currentTimeMillis();
 
-		System.out.println("Runtime " + modelName + ": " + (end - start) + " total, " +
-				(startSmt - start) + " translation, " + (end - startSmt) + " SMT");
+		logInfo("Runtime product-line analysis for " + modelName + ": " + (end - start) +
+				" total, " + (startSmt - start) + " translation, " + (end - startSmt) + " SMT");
 
 		List<ProductLineConstraintViolation> ret = new ArrayList<ProductLineConstraintViolation>();
 
-		if(result.equals(UNSATISFIABLE)) {
-			// No constraint was violated
-
-			// BoolExpr[] unsatCore = solver.getUnsatCore();
-			//
-			// PrintWriter printWriter;
-			//
-			// try {
-			// printWriter = new PrintWriter(
-			// "C:\\Users\\bayha\\tmp\\z3" + modelName + (start % 159739431) + "unsat");
-			//
-			// for(BoolExpr b : unsatCore) {
-			// BoolExpr coreExpr = tracToExpr.get(b);
-			//
-			// printWriter.println(coreExpr);
-			// }
-			//
-			// printWriter.close();
-			// } catch(FileNotFoundException e) {
-			// // TODO Auto-generated catch block
-			// e.printStackTrace();
-			// }
-
-			// System.out.println(deepToString(unsatCore));
-		} else {
-
+		if(result.equals(Status.SATISFIABLE)) {
+			// A violating configuration (i.e. model for negated constraints) was found -> extract
+			// violating model elements.
 			Model z3Model = solver.getModel();
 
 			for(BoolExpr constTrack : constraintTracker2Constraint.keySet()) {
-				Expr constInterp = z3Model.getConstInterp(constTrack);
+				Expr<?> constInterp = z3Model.getConstInterp(constTrack);
 
 				if(constInterp instanceof BoolExpr) {
 					if(constInterp.equals(translation.getContext().mkTrue())) {
@@ -130,8 +97,8 @@ public abstract class GenericProductLineAnalysis {
 								constraintTracker2Constraint.get(constTrack);
 
 						List<EObject> violatingObjects = new ArrayList<EObject>();
-						for(Expr varTrack : failedConstraint.getVariableTracker()) {
-							Expr interpr = z3Model.getConstInterp(varTrack);
+						for(Expr<?> varTrack : failedConstraint.getVariableTracker()) {
+							Expr<?> interpr = z3Model.getConstInterp(varTrack);
 							EObject eObject = translation.getEObjectForExpression(interpr);
 
 							violatingObjects.add(eObject);
@@ -143,16 +110,6 @@ public abstract class GenericProductLineAnalysis {
 				}
 
 			}
-
-			try {
-				PrintWriter printWriter = new PrintWriter(
-						"C:\\Users\\bayha\\tmp\\z3" + modelName + (start % 159739431) + "out");
-				printWriter.println(z3Model);
-				printWriter.close();
-			} catch(FileNotFoundException e) {
-				// TODO Auto-generated catch block
-				e.printStackTrace();
-			}
 		}
 
 		translation.getContext().close();
@@ -160,10 +117,8 @@ public abstract class GenericProductLineAnalysis {
 		return ret;
 	}
 
-	/**
-	 * 
-	 */
-	private void setTranslatedClassesAndReferences() {
+	/** Retrieves the classes, references and attributes required by the constraints. */
+	private void setTranslatedMetamodelElements() {
 		Set<EClass> classes = new HashSet<EClass>();
 		Set<EReference> references = new HashSet<EReference>();
 		Set<EAttribute> attributes = new HashSet<EAttribute>();
@@ -177,8 +132,5 @@ public abstract class GenericProductLineAnalysis {
 		translation.setTranslatedEClasses(classes);
 		translation.setTranslatedEReferences(references);
 		translation.setTranslatedEAttributes(attributes);
-
 	}
-
-	protected abstract void addConstriants();
 }