diff --git a/org.fortiss.tooling.ext.variability/META-INF/MANIFEST.MF b/org.fortiss.tooling.ext.variability/META-INF/MANIFEST.MF
index ee754963c613d328231392486e6104ac8fc1c23d..95570fbc70580acecdd505f77ad336e162773742 100644
--- a/org.fortiss.tooling.ext.variability/META-INF/MANIFEST.MF
+++ b/org.fortiss.tooling.ext.variability/META-INF/MANIFEST.MF
@@ -12,8 +12,9 @@ Bundle-ActivationPolicy: lazy
Bundle-Activator: org.fortiss.tooling.ext.variability.ToolingVariabilityActivator
Require-Bundle: org.fortiss.variability;visibility:=reexport,
org.fortiss.tooling.base
-Export-Package: org.fortiss.tooling.ext.variability.model,
- org.fortiss.tooling.ext.variability.service,
- org.fortiss.tooling.ext.variability.util,
+Export-Package: org.fortiss.tooling.ext.variability.analysis,
+ org.fortiss.tooling.ext.variability.model,
org.fortiss.tooling.ext.variability.model.impl,
- org.fortiss.tooling.ext.variability.model.util
+ org.fortiss.tooling.ext.variability.model.util,
+ org.fortiss.tooling.ext.variability.service,
+ org.fortiss.tooling.ext.variability.util
diff --git a/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/.ratings b/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/.ratings
new file mode 100644
index 0000000000000000000000000000000000000000..b7b707eef8c495baacc3d62d01d79d3d48e5af6e
--- /dev/null
+++ b/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/.ratings
@@ -0,0 +1 @@
+ProductLineTranslation.java 09b5584a67c34c676c97cc1fa073c83ddce23685 YELLOW
diff --git a/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineAnalysis.java b/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineAnalysis.java
new file mode 100644
index 0000000000000000000000000000000000000000..f62987923f99bd4e8fd12b508f0fee94bf564741
--- /dev/null
+++ b/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineAnalysis.java
@@ -0,0 +1,43 @@
+/*-------------------------------------------------------------------------+
+| 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.tooling.ext.variability.analysis;
+
+import org.eclipse.emf.ecore.EObject;
+import org.fortiss.variability.analysis.ProductLineBaseAnalysis;
+import org.fortiss.variability.analysis.ProductLineBaseTranslation;
+
+/**
+ *
+ * @author bayha
+ */
+public class ProductLineAnalysis extends ProductLineBaseAnalysis {
+
+ /**
+ * @param model
+ */
+ public ProductLineAnalysis(EObject model) {
+ this(model, new ProductLineTranslation());
+ }
+
+ /**
+ * @param model
+ * @param translation
+ */
+ protected ProductLineAnalysis(EObject model, ProductLineBaseTranslation translation) {
+ super(model, translation);
+ }
+
+}
diff --git a/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineTranslation.java b/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineTranslation.java
new file mode 100644
index 0000000000000000000000000000000000000000..09b5584a67c34c676c97cc1fa073c83ddce23685
--- /dev/null
+++ b/org.fortiss.tooling.ext.variability/src/org/fortiss/tooling/ext/variability/analysis/ProductLineTranslation.java
@@ -0,0 +1,38 @@
+/*-------------------------------------------------------------------------+
+| 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.tooling.ext.variability.analysis;
+
+import static org.fortiss.tooling.ext.variability.util.VariabilityUtils.calculateGlobalPresenceCondition;
+
+import org.eclipse.emf.ecore.EObject;
+import org.fortiss.tooling.base.model.element.IModelElementSpecification;
+import org.fortiss.variability.analysis.ProductLineBaseTranslation;
+import org.fortiss.variability.model.presence.PresenceConditionTerm;
+
+/**
+ * Adjusts the generic implementation of the translation to the variation point translation with
+ * {@link IModelElementSpecification}s.
+ *
+ * @author bayha
+ */
+public class ProductLineTranslation extends ProductLineBaseTranslation {
+
+ /** {@inheritDoc} */
+ @Override
+ protected PresenceConditionTerm getGlobalPresenceConditionForEObject(EObject eo) {
+ return calculateGlobalPresenceCondition(eo);
+ }
+}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseAnalysis.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseAnalysis.java
new file mode 100644
index 0000000000000000000000000000000000000000..f4433a8d1a28cc36b2618d76e350a4ee5ac39b4a
--- /dev/null
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseAnalysis.java
@@ -0,0 +1,191 @@
+package org.fortiss.variability.analysis;
+
+import static com.microsoft.z3.Status.UNSATISFIABLE;
+import static java.util.Arrays.deepToString;
+import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
+import static org.fortiss.variability.VariabilityActivator.getDefault;
+
+import java.io.FileNotFoundException;
+import java.io.PrintWriter;
+import java.util.ArrayList;
+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.tooling.kernel.model.INamedElement;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.FuncDecl;
+import com.microsoft.z3.Model;
+import com.microsoft.z3.Solver;
+import com.microsoft.z3.Status;
+
+/**
+ * Base class that implements the translation of model product-lines to SMT in order to perform
+ * product-line analysis via constraint lifting.
+ *
+ * @author bayha
+ */
+public class ProductLineBaseAnalysis {
+
+ protected final ProductLineBaseTranslation translation;
+
+ /** List of all translated correctness constraints. */
+ protected List<BoolExpr> constraints = new ArrayList<BoolExpr>();
+
+ protected final EObject model;
+
+ protected Context ctx;
+
+ /**
+ * Constructor.
+ */
+ protected ProductLineBaseAnalysis(EObject model, ProductLineBaseTranslation translation) {
+ this.model = model;
+
+ this.translation = translation;
+ ctx = translation.ctx;
+ }
+
+ /**
+ * Performs a product-line analysis for the given model.
+ *
+ * @return 'true' if all constraints are fulfilled for all variants of the product-line
+ * analysis. 'false' otherwise.
+ */
+ public boolean doCheck() {
+ final long start = System.currentTimeMillis();
+
+ translation.doTranslate(model);
+
+ Solver solver = getSolver();
+
+ 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();
+
+ Status result = solver.check();
+
+ long end = System.currentTimeMillis();
+
+ System.out.println("Runtime " + modelName + ": " + (end - start) + " total, " +
+ (startSmt - start) + " translation, " + (end - startSmt) + " SMT");
+
+ if(result.equals(UNSATISFIABLE)) {
+ BoolExpr[] unsatCore = solver.getUnsatCore();
+
+ PrintWriter printWriter;
+
+ try {
+ printWriter = new PrintWriter(
+ "C:\\Users\\bayha\\tmp\\z3" + modelName + (start % 159739431) + "out");
+
+ 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 {
+ Model z3Model = solver.getModel();
+ 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.ctx.close();
+
+ return result.equals(UNSATISFIABLE);
+ }
+
+ /** Mapping from tracking variables to z3 expression (used for counterexample extraction). */
+ protected Map<BoolExpr, BoolExpr> tracToExpr = new HashMap<BoolExpr, BoolExpr>();
+
+ /** gets the Z3 solver to be used for analysis and adds all constraints. */
+ protected Solver getSolver() {
+ Solver solver = translation.createSolver();
+
+ if(constraints.size() > 0) {
+ solver.add(translation.ctx.mkOr(constraints.toArray(new BoolExpr[constraints.size()])));
+ }
+ return solver;
+ }
+
+ /** Needs to be overwritten to add the constraints to be checked. */
+ protected void translateConstraints() {
+ // EMPTY
+ }
+
+ /** Automatically lifts the given constraint */
+ protected BoolExpr liftConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
+ BoolExpr body, boolean isForAll) {
+ return createLiftedConstraint(quantifierValiables, variableClasses, new BoolExpr[0], body,
+ isForAll);
+ }
+
+ /** Automatically lifts the given constraint */
+ protected BoolExpr createLiftedConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
+ BoolExpr[] containmentExprs, BoolExpr body, boolean isForAll) {
+
+ BoolExpr[] selExprs = new BoolExpr[quantifierValiables.length + containmentExprs.length];
+ for(int i = 0; i < quantifierValiables.length; i++) {
+ EClass cls = variableClasses[i];
+ Expr var = quantifierValiables[i];
+
+ FuncDecl selFun = translation.eClass2SelectionFunction.get(cls);
+ BoolExpr selected = (BoolExpr)ctx.mkApp(selFun, var);
+ BoolExpr notNull = ctx.mkNot(ctx.mkEq(var, translation.eClass2NullElement.get(cls)));
+
+ selExprs[i] = ctx.mkAnd(selected, notNull);
+ }
+
+ // Add containment expressions
+ int j = 0;
+ for(int i = quantifierValiables.length; i < quantifierValiables.length +
+ containmentExprs.length; i++) {
+ selExprs[i] = containmentExprs[j++];
+ }
+
+ if(isForAll) {
+ BoolExpr liftedBody = ctx.mkImplies(ctx.mkAnd(selExprs), body);
+ return ctx.mkForall(quantifierValiables, liftedBody, 0, null, null, null, null);
+ }
+
+ // else: Exits
+ BoolExpr liftedBody = ctx.mkAnd(ctx.mkAnd(selExprs), body);
+ return ctx.mkExists(quantifierValiables, liftedBody, 0, null, null, null, null);
+ }
+
+ /** Logs an error in the analysis. */
+ private void logError(String message) {
+ error(getDefault(), "Error in product-line analysis: " + message);
+ }
+}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseTranslation.java
similarity index 83%
rename from org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineTranslation.java
rename to org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseTranslation.java
index 9139a0e255bd3a06074064afd4b111a61a54de25..9a9444ce68a0774c6377e33f49b58b46441ca0a1 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineTranslation.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseTranslation.java
@@ -1,13 +1,11 @@
package org.fortiss.variability.analysis;
-import static com.microsoft.z3.Status.UNSATISFIABLE;
-import static java.util.Arrays.deepToString;
import static java.util.stream.Collectors.toList;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
+import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
+import static org.fortiss.variability.VariabilityActivator.getDefault;
import static org.fortiss.variability.util.VariabilityUtilsInternal.calculateGlobalPresenceCondition;
-import java.io.FileNotFoundException;
-import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
@@ -25,7 +23,6 @@ import org.eclipse.emf.ecore.EEnumLiteral;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.EReference;
import org.eclipse.emf.ecore.EcorePackage;
-import org.fortiss.tooling.kernel.model.INamedElement;
import org.fortiss.variability.model.features.AbstractAlternativeFeature;
import org.fortiss.variability.model.features.AbstractCrossFeatureConstraint;
import org.fortiss.variability.model.features.AbstractFeature;
@@ -46,12 +43,10 @@ import com.microsoft.z3.EnumSort;
import com.microsoft.z3.Expr;
import com.microsoft.z3.FuncDecl;
import com.microsoft.z3.IntSort;
-import com.microsoft.z3.Model;
import com.microsoft.z3.SeqExpr;
import com.microsoft.z3.SeqSort;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Sort;
-import com.microsoft.z3.Status;
import com.microsoft.z3.StringSymbol;
import com.microsoft.z3.Symbol;
@@ -61,7 +56,7 @@ import com.microsoft.z3.Symbol;
*
* @author bayha
*/
-public class ProductLineTranslation {
+public class ProductLineBaseTranslation {
/** Z3 sort for base type integer. */
protected static IntSort INT_SORT;
@@ -124,8 +119,6 @@ public class ProductLineTranslation {
/** List of all translated assertions for the model. */
protected List<BoolExpr> assertions = new ArrayList<BoolExpr>();
- /** List of all translated correctness constraints. */
- protected List<BoolExpr> constraints = new ArrayList<BoolExpr>();
/** List of all assertions for the feature model. */
protected List<BoolExpr> featureModelAssertions = new ArrayList<BoolExpr>();
/** List of all assertions which encode the presence conditions. */
@@ -134,7 +127,7 @@ public class ProductLineTranslation {
/**
* Constructor.
*/
- protected ProductLineTranslation() {
+ protected ProductLineBaseTranslation() {
initialize();
}
@@ -179,85 +172,8 @@ public class ProductLineTranslation {
}
}
- /**
- * Performs a product-line analysis for the given model.
- *
- * @param model
- * The {@link EObject} which is the model product-line to be analyzed.
- * @return 'true' if all constraints are fulfilled for all variants of the product-line
- * analysis. 'false' otherwise.
- */
- public boolean doCheck(EObject model) {
- final long start = System.currentTimeMillis();
-
- doTranslate(model);
-
- Solver solver = 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();
-
- Status result = solver.check();
-
- long end = System.currentTimeMillis();
-
- System.out.println("Runtime " + modelName + ": " + (end - start) + " total, " +
- (startSmt - start) + " translation, " + (end - startSmt) + " SMT");
-
- if(result.equals(UNSATISFIABLE)) {
- BoolExpr[] unsatCore = solver.getUnsatCore();
-
- PrintWriter printWriter;
-
- try {
- printWriter = new PrintWriter(
- "C:\\Users\\bayha\\tmp\\z3" + modelName + (start % 159739431) + "out");
-
- 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 {
- Model z3Model = solver.getModel();
- 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();
- }
- }
-
- ctx.close();
-
- return result.equals(UNSATISFIABLE);
- }
-
/** Performs the complete translation of the product-line to Z3. */
- private void doTranslate(EObject model) {
+ /* package */ void doTranslate(EObject model) {
// Prepare the core translation
excludeClassesAndReferences();
translateFeatureModel(model);
@@ -272,9 +188,6 @@ public class ProductLineTranslation {
// Model translation
translateObjects();
-
- // Constraint translation
- translateConstraints();
}
/** Translates the presence conditions to Z3. */
@@ -346,7 +259,7 @@ public class ProductLineTranslation {
return ctx.mkNot(translatePresenceCondition(((NotPC)pc).getOperand()));
}
- System.out.println("Unknown Retsriction: " + pc);
+ logError("Unknown PresenceCondition: " + pc);
return null;
}
@@ -455,15 +368,8 @@ public class ProductLineTranslation {
}
solver.assertAndTrack(assertionsArray, assertionsTracArray);
- if(constraints.size() > 0) {
- solver.add(ctx.mkOr(constraints.toArray(new BoolExpr[constraints.size()])));
- }
- return solver;
- }
- /** Needs to be overwritten to add the constraints to be checked. */
- protected void translateConstraints() {
- // EMPTY
+ return solver;
}
/** Translates all objects in the model. */
@@ -571,57 +477,12 @@ public class ProductLineTranslation {
return singleValExpr;
}
- /** Automatically lifts the given constraint */
- protected BoolExpr liftConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
- BoolExpr body, boolean isForAll) {
- return createLiftedConstraint(quantifierValiables, variableClasses, new BoolExpr[0], body,
- isForAll);
- }
-
- /** Automatically lifts the given constraint */
- protected BoolExpr createLiftedConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
- BoolExpr[] containmentExprs, BoolExpr body, boolean isForAll) {
-
- BoolExpr[] selExprs = new BoolExpr[quantifierValiables.length + containmentExprs.length];
- for(int i = 0; i < quantifierValiables.length; i++) {
- EClass cls = variableClasses[i];
- Expr var = quantifierValiables[i];
-
- FuncDecl selFun = eClass2SelectionFunction.get(cls);
- BoolExpr selected = (BoolExpr)ctx.mkApp(selFun, var);
- BoolExpr notNull = ctx.mkNot(ctx.mkEq(var, eClass2NullElement.get(cls)));
-
- selExprs[i] = ctx.mkAnd(selected, notNull);
- }
-
- // Add containment expressions
- int j = 0;
- for(int i = quantifierValiables.length; i < quantifierValiables.length +
- containmentExprs.length; i++) {
- selExprs[i] = containmentExprs[j++];
- }
-
- if(isForAll) {
- BoolExpr liftedBody = ctx.mkImplies(ctx.mkAnd(selExprs), body);
- return ctx.mkForall(quantifierValiables, liftedBody, 0, null, null, null, null);
- }
-
- // else: Exits
- BoolExpr liftedBody = ctx.mkAnd(ctx.mkAnd(selExprs), body);
- return ctx.mkExists(quantifierValiables, liftedBody, 0, null, null, null, null);
-
- }
-
/** Creates a function call with the given expression as a parameter. */
protected Expr createFunctionCallOnExpr(Expr startExpr, String funName, EClass startExprType) {
FuncDecl fun = attRefNames2FuncDecl.get(startExprType, funName);
return ctx.mkApp(fun, startExpr);
}
- // protected Expr createConstraintVar(String name, EClass type) {
- // return ctx.mkConst(name, eClass2Datatype.get(type));
- // }
-
/**
* Creates a containment reference between the given expressions, analogly to the containment in
* EMF.
@@ -662,7 +523,7 @@ public class ProductLineTranslation {
// Single value
if(attType.equals(EcorePackage.Literals.EINT)) {
if(value == null) {
- System.out.println("null int found");
+ logError("null int found");
return ctx.mkInt(0);
}
return ctx.mkInt((int)value);
@@ -675,14 +536,14 @@ public class ProductLineTranslation {
}
if(attType.equals(EcorePackage.Literals.EBOOLEAN)) {
if(value == null) {
- System.out.println("null bool found");
+ logError("null bool found");
return ctx.mkBool(false);
}
return ctx.mkBool((boolean)value);
}
if(attType instanceof EEnum) {
if(value == null) {
- System.out.println("null enum found");
+ logError("null enum found");
}
return eLiteral2Expr.get(value);
}
@@ -849,6 +710,11 @@ public class ProductLineTranslation {
}
}
+ /** Logs an error in the translation. */
+ private void logError(String message) {
+ error(getDefault(), "Error in product-line translation: " + message);
+ }
+
/**
* Checks whether any of the elements in the given {@link Collection} is contained in the given
* set of elements.