Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java (revision 74) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java (revision 75) @@ -6,10 +6,11 @@ import de.uni_hildesheim.sse.model.varModel.Constraint; import de.uni_hildesheim.sse.model.varModel.Project; -import de.uni_hildesheim.sse.model.varModel.datatypes.CustomDatatype; import de.uni_hildesheim.sse.model.varModel.filter.ConstraintFinder; -import de.uni_hildesheim.sse.model.varModel.filter.DatatypeFinder; import de.uni_hildesheim.sse.model.varModel.filter.DeclarationFinder; +import de.uni_hildesheim.sse.model.varModel.filter.DeclarationFinder.VisibilityType; import de.uni_hildesheim.sse.model.varModel.filter.FilterType; -import de.uni_hildesheim.sse.model.varModel.filter.DeclarationFinder.VisibilityType; +import de.uni_hildesheim.sse.trans.Bundle; +import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory; +import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory.EASyLogger; /** @@ -19,4 +20,5 @@ */ public class CNFConverter { + private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(CNFConverter.class, Bundle.ID); /** @@ -43,4 +45,9 @@ // 2. Convert the constraints List constraints = constFinder.getConstraints(); + + int num = 0; + int lastNum = 0; + long ms = 0; + long timeLast = System.currentTimeMillis(); for (int i = 0, n = constraints.size(); i < n; i++) { Constraint constraint = constraints.get(i); @@ -50,8 +57,16 @@ } else { converter.convert(constraint); - if (i % 100 == 0) { - System.out.println("Progress: " + i); - } } + + num++; + ms += System.currentTimeMillis() - timeLast; + timeLast = System.currentTimeMillis(); + while (ms > 5000) { + ms -= 5000; + LOGGER.info("Progress: " + num + "/" + constraints.size() + + " (" + (num - lastNum) + " in last 5 seconds)"); + lastNum = num; + } + /* * Release constraint to deallocate memory. Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 74) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 75) @@ -105,7 +105,7 @@ List parts = new ArrayList(); if (declarationArray.length >= 16) { - System.out.println("Handling big constraint: " + declarationArray.length); +// System.out.println("Handling big constraint: " + declarationArray.length); handleBigConstraint(originalConstraint, declarationArray, config, parts); - System.out.println("Done."); +// System.out.println("Done."); } else { handleSmallConstraint(originalConstraint, declarationArray, config, parts); @@ -192,7 +192,7 @@ for (BigInteger i = new BigInteger("0"); i.compareTo(new BigInteger("2").pow(declarationArray.length)) == -1; i = i.add(new BigInteger("1"))) { - if (i.mod(new BigInteger("1000")).compareTo(new BigInteger("0")) == 0) { - System.out.println(i + "/" + new BigInteger("2").pow(declarationArray.length)); - } +// if (i.mod(new BigInteger("1000")).compareTo(new BigInteger("0")) == 0) { +// System.out.println(i + "/" + new BigInteger("2").pow(declarationArray.length)); +// } boolean[] state = new boolean[declarationArray.length]; for (int j = 0; j < state.length; j++) { Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2.java (revision 74) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2.java (revision 75) @@ -1,5 +1,4 @@ package de.uni_hildesheim.sse.trans.convert; -import java.math.BigInteger; import java.util.List; @@ -22,6 +21,6 @@ * Alternative implementation of {@link MaxTermConverter}, which uses a backtracking algorithm * instead of iteration to find all max terms. - * @author El-Sharkawy - * + * + * @author Adam Krafczyk */ public class MaxTermConverter2 extends MaxTermConverter { @@ -33,5 +32,5 @@ Configuration config, List parts) { - handleBigConstraint(originalConstraint, declarationArray, config, parts); + handleConstraint(originalConstraint, declarationArray, config, parts, 0); } @@ -40,51 +39,82 @@ Configuration config, List parts) { - EvaluationVisitor evalVisitor = new EvaluationVisitor(); - evalVisitor.init(config, null, false, null); - // for each combination of the variables (true or false) - for (BigInteger i = new BigInteger("0"); i.compareTo(new BigInteger("2").pow(declarationArray.length)) == -1; - i = i.add(new BigInteger("1"))) { - if (i.mod(new BigInteger("1000")).compareTo(new BigInteger("0")) == 0) { - System.out.println(i + "/" + new BigInteger("2").pow(declarationArray.length)); - } - boolean[] state = new boolean[declarationArray.length]; - for (int j = 0; j < state.length; j++) { - IDecisionVariable decisionVar = config.getDecision(declarationArray[j]); - /* - * i is a bit-field where each bit represents one variable - * j is the current variable - * To test if variable #j is true check if the bit #j in i is 0 or 1 - */ - if (i.testBit(j)) { - 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); - } - } + handleConstraint(originalConstraint, declarationArray, config, parts, 0); + } + + /** + * Converts a constraint into a CNF formula. + * @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 + * @param var the variable to change + */ + protected void handleConstraint(ConstraintSyntaxTree originalConstraint, + AbstractVariable[] declarationArray, Configuration config, List parts, int var) { + + if (var >= declarationArray.length) { + return; + } + + try { + IDecisionVariable decisionVar = config.getDecision(declarationArray[var]); + + decisionVar.setValue(BooleanValue.TRUE, AssignmentState.ASSIGNED); + if (isFalse(originalConstraint, config)) { + addExpression(parts, declarationArray, var, config); + } else { + handleConstraint(originalConstraint, declarationArray, config, parts, var + 1); } - // 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)); + decisionVar.setValue(BooleanValue.FALSE, AssignmentState.ASSIGNED); + if (isFalse(originalConstraint, config)) { + addExpression(parts, declarationArray, var, config); + } else { + handleConstraint(originalConstraint, declarationArray, config, parts, var + 1); } - // 1 * init() + n * clearResult() is much faster than n * (init() + clear()) - evalVisitor.clearResult(); + decisionVar.setValue(null, AssignmentState.UNDEFINED); + + } catch (ConfigurationException e) { + LOGGER.exception(e); } + } + + /** + * Tests if the boolean expression is false. + * + * @param constraint The {@link ConstraintSyntaxTree} that represents the boolean expression + * @param config the {@link Configuration} that holds the variable states + * + * @return whether the boolean expression is false + */ + private boolean isFalse(ConstraintSyntaxTree constraint, Configuration config) { + EvaluationVisitor evaluationVisitor = new EvaluationVisitor(config, null, false, null); + + constraint.accept(evaluationVisitor); + boolean isFalse = !evaluationVisitor.constraintUndefined() && evaluationVisitor.constraintFailed(); + //evaluationVisitor.clear(); + + return isFalse; + } + + /** + * Adds the boolean expression to the list of expressions. + * + * @param parts The List that the new part is added to + * @param declarationArray Array with all variable declarations + * @param var The number of variables that is defined (0 to var -1 in the declaration array) + * @param config The {@link Configuration} that holds the states of the variables + */ + private void addExpression(List parts, AbstractVariable[] declarationArray, int var, + Configuration config) { + + boolean[] state = new boolean[var + 1]; + for (int i = 0; i < state.length; i++) { + state[i] = ((BooleanValue) config.getDecision(declarationArray[i]).getValue()) == BooleanValue.TRUE; + } + parts.add(createNegatedORExpression(declarationArray, state)); } @@ -103,5 +133,5 @@ } - for (int i = 1; i < variables.length; i++) { + for (int i = 1; i < states.length; i++) { ConstraintSyntaxTree variable = new Variable(variables[i]); if (states[i]) { @@ -112,3 +142,4 @@ return call; } + } Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/AllTests.java =================================================================== --- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/AllTests.java (revision 74) +++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/AllTests.java (revision 75) @@ -8,4 +8,5 @@ import de.uni_hildesheim.sse.trans.convert.DisjunctionCheckerTest; +import de.uni_hildesheim.sse.trans.convert.MaxTermConverter2Test; import de.uni_hildesheim.sse.trans.convert.MaxTermConverterTest; import de.uni_hildesheim.sse.trans.in.ModelReaderTest; @@ -23,4 +24,5 @@ DisjunctionCheckerTest.class, MaxTermConverterTest.class, + MaxTermConverter2Test.class, DimacsWriterTest.class }) Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2Test.java =================================================================== --- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2Test.java (revision 75) +++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2Test.java (revision 75) @@ -0,0 +1,122 @@ +package de.uni_hildesheim.sse.trans.convert; + +import org.junit.Assert; +import org.junit.Test; + +import de.uni_hildesheim.sse.model.cst.CSTSemanticException; +import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree; +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.varModel.Constraint; +import de.uni_hildesheim.sse.model.varModel.DecisionVariableDeclaration; +import de.uni_hildesheim.sse.model.varModel.Project; +import de.uni_hildesheim.sse.model.varModel.datatypes.BooleanType; +import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords; +import de.uni_hildesheim.sse.model.varModel.filter.ConstraintFinder; + +/** + * Tests the {@link MaxTermConverter2}. + * + * @author Adam Krafczyk + */ +public class MaxTermConverter2Test { + + /** + * Tests the convert method. + */ + @Test + public void testConvert() { + DecisionVariableDeclaration declA = new DecisionVariableDeclaration("a", BooleanType.TYPE, null); + DecisionVariableDeclaration declB = new DecisionVariableDeclaration("b", BooleanType.TYPE, null); + DecisionVariableDeclaration declC = new DecisionVariableDeclaration("c", BooleanType.TYPE, null); + + 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) + + Project testProject = new Project("TestProject"); + Constraint constraint = new Constraint(testProject); + try { + constraint.setConsSyntax(completeTerm); + } catch (CSTSemanticException e) { + Assert.fail(e.getMessage()); + } + + new MaxTermConverter2().convert(constraint); + + ConstraintFinder finder = new ConstraintFinder(testProject); + Assert.assertTrue(finder.getConstraints().size() > 0); + for (Constraint c : finder.getConstraints()) { + testConstraintOnlyContainsORandNOT(c.getConsSyntax()); + //c.getConsSyntax().accept(new DebugConstraintTreeVisitor(System.out)); + } + } + + /** + * Tests whether a constraint only contains OR's and NOT's. + * @param tree The constraint to be tested. + */ + private void testConstraintOnlyContainsORandNOT(ConstraintSyntaxTree tree) { + if (tree instanceof OCLFeatureCall) { + OCLFeatureCall call = (OCLFeatureCall) tree; + Assert.assertTrue(call.getOperation().equals(OclKeyWords.OR) + || call.getOperation().equals(OclKeyWords.NOT)); + testConstraintOnlyContainsORandNOT(call.getOperand()); + } + } + + /** + * Tests the convert method with a constraint with more than 15 variables. + */ + @Test + public void testConvertWithBigConstraint() { + Variable[] vars = new Variable[18]; + for (int i = 0; i < vars.length; i++) { + vars[i] = new Variable(new DecisionVariableDeclaration((char) ('a' + i) + "", BooleanType.TYPE, null)); + } + + ConstraintSyntaxTree term = vars[0]; + for (int i = 1; i < vars.length; i++) { + if (Math.random() > 0.5) { + term = new OCLFeatureCall(term, OclKeyWords.OR, vars[i]); + } else { + term = new OCLFeatureCall(term, OclKeyWords.OR, new OCLFeatureCall(vars[i], OclKeyWords.NOT)); + } + } + + Project testProject = new Project("TestProject"); + Constraint constraint = new Constraint(testProject); + try { + constraint.setConsSyntax(term); + } catch (CSTSemanticException e) { + Assert.fail(e.getMessage()); + } + + new MaxTermConverter2().convert(constraint); + + ConstraintFinder finder = new ConstraintFinder(testProject); + Assert.assertTrue(finder.getConstraints().size() > 0); + for (Constraint c : finder.getConstraints()) { + testConstraintOnlyContainsORandNOT(c.getConsSyntax()); + } + } + +} Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java =================================================================== --- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java (revision 74) +++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java (revision 75) @@ -69,6 +69,8 @@ ConstraintFinder finder = new ConstraintFinder(testProject); + Assert.assertTrue(finder.getConstraints().size() > 0); for (Constraint c : finder.getConstraints()) { testConstraintOnlyContainsORandNOT(c.getConsSyntax()); +// c.getConsSyntax().accept(new DebugConstraintTreeVisitor(System.out)); } } @@ -117,4 +119,5 @@ ConstraintFinder finder = new ConstraintFinder(testProject); + Assert.assertTrue(finder.getConstraints().size() > 0); for (Constraint c : finder.getConstraints()) { testConstraintOnlyContainsORandNOT(c.getConsSyntax());