Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 61)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 62)
@@ -30,4 +30,5 @@
* max terms.
* @author Adam Krafczyk
+ * @author El-Sharkawy
*
*/
@@ -87,53 +88,75 @@
System.out.println("Skipping too long Constraint");
} else {
- for (int i = 0; i < Math.pow(2, declarationArray.length); i++) {
- boolean[] state = new boolean[declarationArray.length];
- for (int j = 0; j < state.length; j++) {
- IDecisionVariable decisionVar = config.getDecision(declarationArray[j]);
- if ((i & (1 << j)) != 0) {
- state[j] = true;
- try {
- decisionVar.setValue(BooleanValue.TRUE, AssignmentState.ASSIGNED);
- } catch (ConfigurationException e) {
- // TODO
- LOGGER.exception(e);
- }
- } else {
- state[j] = false;
- try {
- decisionVar.setValue(BooleanValue.FALSE, AssignmentState.ASSIGNED);
- } catch (ConfigurationException e) {
- // TODO
- LOGGER.exception(e);
- }
+ handleSmallConstraint(originalConstraint, declarationArray, config, parts);
+ }
+
+ return parts;
+ }
+
+ /**
+ * Converts a small constraint into a CNF formula.
+ * This constraint must have at maximum 15 different {@link AbstractVariable}s.
+ * @param originalConstraint The constraint which shall be converted into CNF formula.
+ * this constraint may consists only of AND, OR, and NOT operations.
+ * @param declarationArray The {@link AbstractVariable}s, which are used inside the originalConstraint.
+ * @param config A temporary {@link Configuration} containing only originalConstraint
+ * and declarationArray
+ * @param parts An empty list, where the resulting disjunctions terms of the CNF formula shall be added to
+ */
+ protected void handleSmallConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray,
+ Configuration config, List parts) {
+
+ EvaluationVisitor evalVisitor = new EvaluationVisitor();
+ evalVisitor.init(config, null, false, null);
+ for (int i = 0; i < Math.pow(2, declarationArray.length); i++) {
+ boolean[] state = new boolean[declarationArray.length];
+ for (int j = 0; j < state.length; j++) {
+ IDecisionVariable decisionVar = config.getDecision(declarationArray[j]);
+ if ((i & (1 << j)) != 0) {
+ state[j] = true;
+ try {
+ decisionVar.setValue(BooleanValue.TRUE, AssignmentState.ASSIGNED);
+ } catch (ConfigurationException e) {
+ // TODO
+ LOGGER.exception(e);
+ }
+ } else {
+ state[j] = false;
+ try {
+ decisionVar.setValue(BooleanValue.FALSE, AssignmentState.ASSIGNED);
+ } catch (ConfigurationException e) {
+ // TODO
+ LOGGER.exception(e);
}
}
-
- // get the result
- boolean result = getResult(originalConstraint, config);
-
- // if the result it false, add the negated combination to the list of expressions
- if (!result) {
- parts.add(createNegatedORExpression(declarationArray, state));
- }
- }
- }
-
- return parts;
- }
-
- /**
- * Returns whether the boolean expression with the given variable states is true or false.
- * @param expression The boolean expression
- * @param config The {@link Configuration} that defines the state of the variables
- * @return The result of the boolean expression
- */
- private boolean getResult(ConstraintSyntaxTree expression, Configuration config) {
- EvaluationVisitor evalVisitor = new EvaluationVisitor();
- evalVisitor.init(config, null, false, null);
- expression.accept(evalVisitor);
- BooleanValue result = (BooleanValue) evalVisitor.getResult();
- return result.equals(BooleanValue.TRUE);
- }
+ }
+
+ // get the result
+ originalConstraint.accept(evalVisitor);
+ boolean result = evalVisitor.constraintFulfilled();
+
+ // if the result it false, add the negated combination to the list of expressions
+ if (!result) {
+ parts.add(createNegatedORExpression(declarationArray, state));
+ }
+
+ // 1 * init() + n * clearResult() is much faster than n * (init() + clear())
+ evalVisitor.clearResult();
+ }
+ }
+
+// /**
+// * Returns whether the boolean expression with the given variable states is true or false.
+// * @param expression The boolean expression
+// * @param config The {@link Configuration} that defines the state of the variables
+// * @return The result of the boolean expression
+// */
+// private boolean getResult(ConstraintSyntaxTree expression, Configuration config) {
+// EvaluationVisitor evalVisitor = new EvaluationVisitor();
+// evalVisitor.init(config, null, false, null);
+// expression.accept(evalVisitor);
+// BooleanValue result = (BooleanValue) evalVisitor.getResult();
+// return result.equals(BooleanValue.TRUE);
+// }
/**
Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java
===================================================================
--- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java (revision 61)
+++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java (revision 62)
@@ -2,10 +2,15 @@
import org.junit.Assert;
+import org.junit.Ignore;
import org.junit.Test;
+import de.uni_hildesheim.sse.model.confModel.AssignmentState;
+import de.uni_hildesheim.sse.model.confModel.Configuration;
+import de.uni_hildesheim.sse.model.confModel.ConfigurationException;
import de.uni_hildesheim.sse.model.cst.CSTSemanticException;
import de.uni_hildesheim.sse.model.cst.OCLFeatureCall;
import de.uni_hildesheim.sse.model.cst.Parenthesis;
import de.uni_hildesheim.sse.model.cst.Variable;
+import de.uni_hildesheim.sse.model.cstEvaluation.EvaluationVisitor;
import de.uni_hildesheim.sse.model.varModel.Constraint;
import de.uni_hildesheim.sse.model.varModel.DecisionVariableDeclaration;
@@ -14,4 +19,5 @@
import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords;
import de.uni_hildesheim.sse.model.varModel.filter.ConstraintFinder;
+import de.uni_hildesheim.sse.model.varModel.values.BooleanValue;
/**
@@ -56,4 +62,5 @@
try {
constraint.setConsSyntax(completeTerm);
+ //testProject.add(constraint);
} catch (CSTSemanticException e) {
Assert.fail(e.getMessage());
@@ -69,4 +76,63 @@
Assert.assertEquals(4, finder.getConstraints().size());
}
+
+ /**
+ * Tests whether the {@link EvaluationVisitor}, which is used inside of {@link MaxTermConverter}, is sufficient
+ * for {@link MaxTermConverter}.
+ */
+ @Ignore()
+ @Test
+ public void testEvaluationVisitor() {
+ Project testProject = new Project("TestProject");
+ DecisionVariableDeclaration declA = new DecisionVariableDeclaration("a", BooleanType.TYPE, testProject);
+ DecisionVariableDeclaration declB = new DecisionVariableDeclaration("b", BooleanType.TYPE, testProject);
+ DecisionVariableDeclaration declC = new DecisionVariableDeclaration("c", BooleanType.TYPE, testProject);
+ testProject.add(declA);
+ testProject.add(declB);
+ testProject.add(declC);
+
+ Variable varB = new Variable(declB);
+ OCLFeatureCall notB = new OCLFeatureCall(varB, OclKeyWords.NOT);
+ OCLFeatureCall termA = new OCLFeatureCall(new Variable(declA), OclKeyWords.OR, varB);
+ OCLFeatureCall termB = new OCLFeatureCall(new Variable(declC), OclKeyWords.OR, notB);
+ Parenthesis parenthesis = new Parenthesis(termB);
+ OCLFeatureCall completeTerm = new OCLFeatureCall(termA, OclKeyWords.AND, parenthesis);
+
+ // (a OR b) AND (c OR !b)
+ /*
+ * a b c r
+ * 0 0 0 0
+ * 1 0 0 1
+ * 0 1 0 0
+ * 1 1 0 0
+ * 0 0 1 0
+ * 1 0 1 1
+ * 0 1 1 1
+ * 1 1 1 1
+ */
+ // (a OR b OR c) AND (a OR !b OR c) AND (!a OR !b OR c) AND (a OR b OR !c)
+ Constraint constraint = new Constraint(testProject);
+ try {
+ constraint.setConsSyntax(completeTerm);
+ testProject.add(constraint);
+ } catch (CSTSemanticException e) {
+ Assert.fail(e.getMessage());
+ }
+
+ Configuration config = new Configuration(testProject);
+ try {
+ config.getDecision(declB).setValue(BooleanValue.TRUE, AssignmentState.ASSIGNED);
+ config.getDecision(declC).setValue(BooleanValue.FALSE, AssignmentState.ASSIGNED);
+ } catch (ConfigurationException e) {
+ Assert.fail(e.getMessage());
+ }
+ EvaluationVisitor evaluator = new EvaluationVisitor(config, null, false, null);
+ completeTerm.accept(evaluator);
+
+ System.out.println(evaluator.constraintFailed());
+ System.out.println(evaluator.constraintFulfilled());
+ System.out.println(evaluator.constraintUndefined());
+ Assert.assertTrue(evaluator.constraintFailed());
+ }
}