From 5dc344cfcd5ce7fa1465570b5947e0d21321340d Mon Sep 17 00:00:00 2001
From: Andreas Bayha <bayha@fortiss.org>
Date: Fri, 21 Apr 2023 18:13:58 +0200
Subject: [PATCH] Variability: Added extraction of counterexample to
ProductLineAnalysis
The analysis has been refined with meaningful violations as a result.
Those include the violating objects, the constraints and (once
implemented) the violating feature configuration.
Issue-ref: 4240
Issue-URL: af3#4240
Signed-off-by: Andreas Bayha <bayha@fortiss.org>
---
.../analysis/IProductLineConstraint.java | 50 +++++++
.../analysis/ProductLineBaseAnalysis.java | 129 +++++++++++++++---
.../analysis/ProductLineBaseTranslation.java | 59 ++++----
.../ProductLineConstraintViolation.java | 66 +++++++++
4 files changed, 257 insertions(+), 47 deletions(-)
create mode 100644 org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java
create mode 100644 org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintViolation.java
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java
new file mode 100644
index 000000000..47d009b35
--- /dev/null
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineConstraint.java
@@ -0,0 +1,50 @@
+/*-------------------------------------------------------------------------+
+| 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.List;
+
+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.Expr;
+
+/**
+ *
+ * @author bayha
+ */
+public interface IProductLineConstraint {
+
+ public String getConstraintName();
+
+ public String getConstraintMessage(List<EObject> violatingObjects,
+ VariantConfiguration violatingConfiguration);
+
+ public Expr[] getQuantifierVariables();
+
+ public EClass[] getVariablesClasses();
+
+ public BoolExpr[] getContainmentExpr();
+
+ public BoolExpr getBody();
+
+ public boolean isForAll();
+
+ public List<Expr> getVariableTracker();
+
+}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseAnalysis.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseAnalysis.java
index ee3aaba5a..ef9785f44 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseAnalysis.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseAnalysis.java
@@ -1,7 +1,6 @@
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;
@@ -35,7 +34,14 @@ public class ProductLineBaseAnalysis {
protected final ProductLineBaseTranslation translation;
/** List of all translated correctness constraints. */
- protected List<BoolExpr> constraints = new ArrayList<BoolExpr>();
+ protected List<BoolExpr> rawConstraints = new ArrayList<BoolExpr>();
+
+ protected List<BoolExpr> constraintTrackers = new ArrayList<BoolExpr>();
+
+ protected List<IProductLineConstraint> plConstraints = new ArrayList<IProductLineConstraint>();
+
+ protected Map<Expr, IProductLineConstraint> constraintTracker2Constraint =
+ new HashMap<Expr, IProductLineConstraint>();
protected final EObject model;
@@ -57,13 +63,17 @@ public class ProductLineBaseAnalysis {
* @return 'true' if all constraints are fulfilled for all variants of the product-line
* analysis. 'false' otherwise.
*/
- public boolean doCheck() {
+ public final List<ProductLineConstraintViolation> doCheck() {
final long start = System.currentTimeMillis();
translation.doTranslate(model);
+ addConstriants();
+
translateConstraints();
+ addRawConstraints();
+
Solver solver = getSolver();
String modelName = ((INamedElement)model).getName();
@@ -88,30 +98,59 @@ public class ProductLineBaseAnalysis {
System.out.println("Runtime " + modelName + ": " + (end - start) + " total, " +
(startSmt - start) + " translation, " + (end - startSmt) + " SMT");
+ List<ProductLineConstraintViolation> ret = new ArrayList<ProductLineConstraintViolation>();
+
if(result.equals(UNSATISFIABLE)) {
- BoolExpr[] unsatCore = solver.getUnsatCore();
+ // No constraint was violated
+
+ // 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();
- PrintWriter printWriter;
+ for(BoolExpr constTrack : constraintTrackers) {
+ Expr constInterp = z3Model.getConstInterp(constTrack);
- try {
- printWriter = new PrintWriter(
- "C:\\Users\\bayha\\tmp\\z3" + modelName + (start % 159739431) + "out");
+ if(constInterp instanceof BoolExpr) {
+ if(constInterp.equals(ctx.mkTrue())) {
+ IProductLineConstraint failedConstraint =
+ constraintTracker2Constraint.get(constTrack);
+
+ List<EObject> violatingObjects = new ArrayList<EObject>();
+ for(Expr varTrack : failedConstraint.getVariableTracker()) {
+ Expr interpr = z3Model.getConstInterp(varTrack);
+ EObject eObject = translation.getExpr2EObject().get(interpr);
- for(BoolExpr b : unsatCore) {
- BoolExpr coreExpr = tracToExpr.get(b);
+ violatingObjects.add(eObject);
+ }
- printWriter.println(coreExpr);
+ ret.add(new ProductLineConstraintViolation(failedConstraint,
+ violatingObjects, null));
+ }
}
- 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");
@@ -125,7 +164,7 @@ public class ProductLineBaseAnalysis {
translation.ctx.close();
- return result.equals(UNSATISFIABLE);
+ return ret;
}
/** Mapping from tracking variables to z3 expression (used for counterexample extraction). */
@@ -135,17 +174,45 @@ public class ProductLineBaseAnalysis {
protected Solver getSolver() {
Solver solver = translation.createSolver();
- if(constraints.size() > 0) {
- solver.add(translation.ctx.mkOr(constraints.toArray(new BoolExpr[constraints.size()])));
+ if(rawConstraints.size() > 0) {
+ solver.add(rawConstraints.toArray(new BoolExpr[rawConstraints.size()]));
+
+ solver.add(translation.ctx
+ .mkOr(constraintTrackers.toArray(new BoolExpr[constraintTrackers.size()])));
}
return solver;
}
/** Needs to be overwritten to add the constraints to be checked. */
- protected void translateConstraints() {
+ protected void addRawConstraints() {
// EMPTY
}
+ protected void addConstriants() {
+ // EMPTY
+ }
+
+ protected void translateConstraints() {
+ for(IProductLineConstraint constraint : plConstraints) {
+ Expr[] quantifierValiables = constraint.getQuantifierVariables();
+ EClass[] variableClasses = constraint.getVariablesClasses();
+ BoolExpr[] containmentExprs = constraint.getContainmentExpr();
+ BoolExpr body = constraint.getBody();
+
+ boolean isForAll = constraint.isForAll();
+
+ BoolExpr quantifier = createLiftedConstraint(quantifierValiables, variableClasses,
+ containmentExprs, body, isForAll);
+
+ BoolExpr constraintTracker =
+ ctx.mkBoolConst("CONSTRAINT_" + constraint.getConstraintName());
+ constraintTracker2Constraint.put(constraintTracker, constraint);
+
+ rawConstraints.add(ctx.mkEq(constraintTracker, quantifier));
+ constraintTrackers.add(constraintTracker);
+ }
+ }
+
/** Automatically lifts the given constraint */
protected BoolExpr liftConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
BoolExpr body, boolean isForAll) {
@@ -153,6 +220,24 @@ public class ProductLineBaseAnalysis {
isForAll);
}
+ // protected BoolExpr createLiftedQuantifier(String[] quantifierValiableNames,
+ // EClass[] variableClasses, BoolExpr[] containmentExprs, BoolExpr body,
+ // boolean isForAll) {
+ //
+ // int numVar = quantifierValiableNames.length;
+ // Expr[] quantifierValiables = new Expr[numVar];
+ //
+ // for(int i = 0; i < numVar; i++) {
+ // EnumSort sort = translation.geteClass2Datatype().get(variableClasses[i]);
+ // Expr expr = ctx.mkConst(quantifierValiableNames[i], sort);
+ //
+ // quantifierValiables[i] = expr;
+ // }
+ //
+ // return createLiftedConstraint(quantifierValiables, variableClasses, containmentExprs, body,
+ // isForAll);
+ // }
+
/** Automatically lifts the given constraint */
protected BoolExpr createLiftedConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
BoolExpr[] containmentExprs, BoolExpr body, boolean isForAll) {
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseTranslation.java
index c3a71c219..56476d967 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseTranslation.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineBaseTranslation.java
@@ -59,11 +59,11 @@ import com.microsoft.z3.Symbol;
public class ProductLineBaseTranslation {
/** Z3 sort for base type integer. */
- protected static IntSort INT_SORT;
+ protected IntSort intSort;
/** Z3 sort for base type string. */
- protected static SeqSort STRING_SORT;
+ protected SeqSort stringSort;
/** Z3 sort for base type boolean. */
- protected static BoolSort BOOL_SORT;
+ protected BoolSort boolSort;
/** Mapping from classes to all their objects */
protected BucketSetMap<EClass, EObject> allObjects = new BucketSetMap<EClass, EObject>();
@@ -105,6 +105,9 @@ public class ProductLineBaseTranslation {
*/
protected DualKeyMap<EObject, EClass, Expr> eObject2Expr =
new DualKeyMap<EObject, EClass, Expr>();
+
+ protected Map<Expr, EObject> expr2EObject = new HashMap<Expr, EObject>();
+
/** Mapping of enumeration literals to the translated Z3 expression. */
protected Map<Enum<?>, Expr> eLiteral2Expr = new HashMap<Enum<?>, Expr>();
/** Mapping of classes to their respective z3 expression for 'null' */
@@ -124,7 +127,7 @@ public class ProductLineBaseTranslation {
protected Context ctx = new Context();
/** List of all translated assertions for the model. */
- protected List<BoolExpr> assertions = new ArrayList<BoolExpr>();
+ protected List<BoolExpr> modelAssertions = 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. */
@@ -142,27 +145,32 @@ public class ProductLineBaseTranslation {
return eClass2Datatype;
}
- // /** Returns eReference2FunDecl. */
- // public DualKeyMap<EReference, EClass, FuncDecl> geteReference2FunDecl() {
- // return eReference2FunDecl;
- // }
-
/** Returns attRefNames2FuncDecl. */
public DualKeyMap<EClass, String, FuncDecl> getAttRefNames2FuncDecl() {
return attRefNames2FuncDecl;
}
+ /** Returns boolSort. */
+ public BoolSort getBoolSort() {
+ return boolSort;
+ }
+
+ /** Returns expr2EObject. */
+ public Map<Expr, EObject> getExpr2EObject() {
+ return expr2EObject;
+ }
+
/**
* Initialization of analysis and base types.
*/
private void initialize() {
- INT_SORT = ctx.mkIntSort();
- STRING_SORT = ctx.mkStringSort();
- BOOL_SORT = ctx.mkBoolSort();
+ intSort = ctx.mkIntSort();
+ stringSort = ctx.mkStringSort();
+ boolSort = ctx.mkBoolSort();
- eDataType2Sort.put(EcorePackage.Literals.EINT, INT_SORT);
- eDataType2Sort.put(EcorePackage.Literals.ESTRING, STRING_SORT);
- eDataType2Sort.put(EcorePackage.Literals.EBOOLEAN, BOOL_SORT);
+ eDataType2Sort.put(EcorePackage.Literals.EINT, intSort);
+ eDataType2Sort.put(EcorePackage.Literals.ESTRING, stringSort);
+ eDataType2Sort.put(EcorePackage.Literals.EBOOLEAN, boolSort);
}
/** Traverses the model to collect all classes and objects to be translated. */
@@ -215,7 +223,7 @@ public class ProductLineBaseTranslation {
protected void translatePresenceConditions() {
for(EClass ec : allObjects.keySet()) {
EnumSort ecSort = eClass2Datatype.get(ec);
- FuncDecl selFun = ctx.mkFuncDecl("SELECTED_" + ec.getName(), ecSort, BOOL_SORT);
+ FuncDecl selFun = ctx.mkFuncDecl("SELECTED_" + ec.getName(), ecSort, boolSort);
eClass2SelectionFunction.put(ec, selFun);
for(EObject eo : allObjects.get(ec)) {
@@ -380,13 +388,13 @@ public class ProductLineBaseTranslation {
solver.add(presenceConditionAssertions
.toArray(new BoolExpr[presenceConditionAssertions.size()]));
// solver.add(assertions.toArray(new BoolExpr[assertions.size()]));
- BoolExpr[] assertionsArray = assertions.toArray(new BoolExpr[assertions.size()]);
- List<BoolExpr> tracList = assertions.stream()
+ BoolExpr[] assertionsArray = modelAssertions.toArray(new BoolExpr[modelAssertions.size()]);
+ List<BoolExpr> tracList = modelAssertions.stream()
.map(a -> ctx.mkBoolConst("tracVar" + a.getId())).collect(toList());
- BoolExpr[] assertionsTracArray = tracList.toArray(new BoolExpr[assertions.size()]);
+ BoolExpr[] assertionsTracArray = tracList.toArray(new BoolExpr[modelAssertions.size()]);
- for(int i = 0; i < assertions.size(); i++) {
- tracToExpr.put(tracList.get(i), assertions.get(i));
+ for(int i = 0; i < modelAssertions.size(); i++) {
+ tracToExpr.put(tracList.get(i), modelAssertions.get(i));
}
solver.assertAndTrack(assertionsArray, assertionsTracArray);
@@ -409,7 +417,7 @@ public class ProductLineBaseTranslation {
Expr attVal = translateAttributeValue(eo, ea);
BoolExpr attValAssertion =
ctx.mkEq(ctx.mkApp(attFunc, eObject2Expr.get(eo, ec)), attVal);
- assertions.add(attValAssertion);
+ modelAssertions.add(attValAssertion);
}
}
}
@@ -422,17 +430,17 @@ public class ProductLineBaseTranslation {
Expr eoExpr = eObject2Expr.get(eo, ec);
Expr refVal = translateReferenceValue(eo, er);
BoolExpr rafValAssertion = ctx.mkEq(ctx.mkApp(refFunc, eoExpr), refVal);
- assertions.add(rafValAssertion);
+ modelAssertions.add(rafValAssertion);
}
// Null must always only point to null....
EClass refType = er.getEReferenceType();
Expr nullElement = eClass2NullElement.get(ec);
if(er.getUpperBound() > 0) {
- assertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
+ modelAssertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
eClass2NullElement.get(refType)));
} else {
- assertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
+ modelAssertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
ctx.mkEmptySeq(eReference2Sort.get(er))));
}
}
@@ -741,6 +749,7 @@ public class ProductLineBaseTranslation {
Expr[] consts = enumSort.getConsts();
for(int i = 0; i < objs.size(); i++) {
eObject2Expr.put(objs.get(i), cls, consts[i]);
+ expr2EObject.put(consts[i], objs.get(i));
}
Expr noneExpr = consts[consts.length - 1];
eClass2NullElement.put(cls, noneExpr);
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintViolation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintViolation.java
new file mode 100644
index 000000000..7d4de79b3
--- /dev/null
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/ProductLineConstraintViolation.java
@@ -0,0 +1,66 @@
+/*-------------------------------------------------------------------------+
+| 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.List;
+
+import org.eclipse.emf.ecore.EObject;
+import org.fortiss.variability.model.features.configuration.VariantConfiguration;
+
+/**
+ *
+ * @author bayha
+ */
+public class ProductLineConstraintViolation {
+
+ protected List<EObject> violatingElements;
+
+ protected IProductLineConstraint constraint;
+
+ private VariantConfiguration violatingConfiguration;
+
+ /**
+ * @param constraint
+ * @param violatingElements
+ * @param violatingConfiguration
+ */
+ public ProductLineConstraintViolation(IProductLineConstraint constraint,
+ List<EObject> violatingElements, VariantConfiguration violatingConfiguration) {
+ this.constraint = constraint;
+ this.violatingElements = violatingElements;
+ this.violatingConfiguration = violatingConfiguration;
+ }
+
+ /** Returns violatingElements. */
+ public List<EObject> getViolatingElements() {
+ return violatingElements;
+ }
+
+ /** Returns errorMessage. */
+ public String getErrorMessage() {
+ return constraint.getConstraintMessage(violatingElements, violatingConfiguration);
+ }
+
+ /** Returns constraint. */
+ public IProductLineConstraint getConstraint() {
+ return constraint;
+ }
+
+ /** Returns violatingConfiguration. */
+ public VariantConfiguration getViolatingConfiguration() {
+ return violatingConfiguration;
+ }
+}
--
GitLab