Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java (revision 59) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java (revision 60) @@ -12,4 +12,5 @@ import de.uni_hildesheim.sse.trans.in.InputType; import de.uni_hildesheim.sse.trans.in.ModelReader; +import de.uni_hildesheim.sse.trans.out.DimacsWriter; import de.uni_hildesheim.sse.trans.out.IModelWriter; import de.uni_hildesheim.sse.trans.out.IVMLWriter; @@ -81,4 +82,13 @@ case DIMCAS: CNFConverter.convert(model, new MaxTermConverter()); + System.out.println("Conversion completed."); + writer = new DimacsWriter(model, out); + writer.write(comment, version); + try { + out.flush(); + out.close(); + } catch (IOException e) { + LOGGER.exception(e); + } break; default: Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java (revision 59) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CNFConverter.java (revision 60) @@ -39,4 +39,5 @@ // 2. Convert the constraints List constraints = constFinder.getConstraints(); + int num = 0; for (Constraint constraint : constraints) { DisjunctionChecker checker = new DisjunctionChecker(constraint); @@ -45,4 +46,8 @@ } else { converter.convert(constraint); + num++; + if (num % 100 == 0) { + System.out.println("Progress: " + num); + } } } Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 59) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 60) @@ -1,12 +1,25 @@ package de.uni_hildesheim.sse.trans.convert; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Comparator; +import java.util.List; import java.util.Set; +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.confModel.IDecisionVariable; 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.Variable; +import de.uni_hildesheim.sse.model.cstEvaluation.EvaluationVisitor; import de.uni_hildesheim.sse.model.varModel.AbstractVariable; import de.uni_hildesheim.sse.model.varModel.Constraint; import de.uni_hildesheim.sse.model.varModel.Project; +import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords; import de.uni_hildesheim.sse.model.varModel.filter.DeclrationInConstraintFinder; +import de.uni_hildesheim.sse.model.varModel.values.BooleanValue; import de.uni_hildesheim.sse.trans.Bundle; import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory; @@ -16,5 +29,5 @@ * Converts a boolean formula in a list of disjunction terms by means of * max terms. - * @author El-Sharkawy + * @author Adam Krafczyk * */ @@ -27,8 +40,123 @@ public void convert(Constraint constraint) { project = (Project) constraint.getTopLevelParent(); + + List parts = createCNFParts(constraint); + for (ConstraintSyntaxTree part : parts) { + addConstraint(part); + } + } + + /** + * Creates a list of parts of CNF for the given {@link Constraint}. + * @param constraint A boolean expression + * @return List of parts of CNF (boolean expressions with OR and NOT). + */ + private List createCNFParts(Constraint constraint) { + // Get an array of all variables in the constraint ConstraintSyntaxTree originalConstraint = constraint.getConsSyntax(); DeclrationInConstraintFinder finder = new DeclrationInConstraintFinder(originalConstraint); Set declarations = finder.getDeclarations(); - System.out.println(declarations.size()); + AbstractVariable[] declarationArray = declarations.toArray(new AbstractVariable[] {}); + Arrays.sort(declarationArray, new Comparator() { + public int compare(AbstractVariable o1, AbstractVariable o2) { + return o1.getName().compareTo(o2.getName()); + } + }); + + // Create a project which only contains our single Constraint + Project singleConstraintProject = new Project("SingleConstraintProject"); + Constraint constraintCopy = null; + try { + constraintCopy = new Constraint(originalConstraint, singleConstraintProject); + } catch (CSTSemanticException e) { + // TODO (can this even happen?) + LOGGER.exception(e); + } + singleConstraintProject.add(constraintCopy); + for (AbstractVariable var : declarationArray) { + singleConstraintProject.add(var); + } + + // Create a configuration object for the singleConstraintProject + Configuration config = new Configuration(singleConstraintProject); + + List parts = new ArrayList(); + // for each combination of the variables (true or false) + // TODO: only works for up to 16 vars + if (declarationArray.length >= 16) { + 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); + } + } + } + + // 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); + } + + /** + * Creates an {@link ConstraintSyntaxTree} with the variables negated and OR'd together. + * @param variables Array of Variables + * @param states Array whether each variable is true or false + * @return the {@link ConstraintSyntaxTree} + */ + private ConstraintSyntaxTree createNegatedORExpression(AbstractVariable[] variables, boolean[] states) { + ConstraintSyntaxTree call = null; + if (!states[0]) { + call = new Variable(variables[0]); + } else { + call = new OCLFeatureCall(new Variable(variables[0]), OclKeyWords.NOT); + } + + for (int i = 1; i < variables.length; i++) { + ConstraintSyntaxTree variable = new Variable(variables[i]); + if (states[i]) { + variable = new OCLFeatureCall(variable, OclKeyWords.NOT); + } + call = new OCLFeatureCall(call, OclKeyWords.OR, variable); + } + return call; } Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/out/DimacsWriter.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/out/DimacsWriter.java (revision 59) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/out/DimacsWriter.java (revision 60) @@ -2,5 +2,5 @@ import java.io.IOException; -import java.io.PrintStream; +import java.io.Writer; import java.util.Collections; import java.util.Comparator; @@ -9,31 +9,111 @@ import java.util.Map; -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.confModel.IDecisionVariable; -import de.uni_hildesheim.sse.model.cstEvaluation.EvaluationVisitor; +import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree; import de.uni_hildesheim.sse.model.varModel.AbstractVariable; import de.uni_hildesheim.sse.model.varModel.Constraint; +import de.uni_hildesheim.sse.model.varModel.IvmlKeyWords; import de.uni_hildesheim.sse.model.varModel.Project; import de.uni_hildesheim.sse.model.varModel.filter.ConstraintFinder; 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.DeclrationInConstraintFinder; import de.uni_hildesheim.sse.model.varModel.filter.FilterType; -import de.uni_hildesheim.sse.model.varModel.values.BooleanValue; +import de.uni_hildesheim.sse.trans.Bundle; +import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory; +import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory.EASyLogger; -public class DimacsWriter { - +/** + * Writer to write the given project into the DIMACS format. + * Only works on projects that have their constraints in CNF. + * + * @author Adam Krafcyk + */ +public class DimacsWriter implements IModelWriter { + private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(DimacsWriter.class, Bundle.ID); + private Project project; private Map variables; + private Writer writer; - public DimacsWriter(Project project) { + /** + * Creates the writer for the given project. + * @param project The project which shall be saved. + * @param writer Writer which should be used for writing the output. + */ + public DimacsWriter(Project project, Writer writer) { this.project = project; + this.writer = writer; variables = new HashMap(); } - public void write(PrintStream out) throws IOException { + /** + * Writes the DIMACS format to the {@link Writer}. + * @throws IOException If writing to the stream fails + */ + public void write() throws IOException { + // Get all variables DeclarationFinder declarationFinder = new DeclarationFinder(project, FilterType.ALL, null); + List variableDeclarations = declarationFinder.getVariableDeclarations(VisibilityType.ALL); + Collections.sort(variableDeclarations, new Comparator() { + public int compare(AbstractVariable o1, AbstractVariable o2) { + return o1.getName().compareTo(o2.getName()); + } + }); + + // Get all Constraints + ConstraintFinder constraintFinder = new ConstraintFinder(project); + List constraints = constraintFinder.getConstraints(); + + // Write variables + Integer i = 1; + for (AbstractVariable variable : variableDeclarations) { + variables.put(variable.getName(), i++); + writer.append("c "); + writer.append(i.toString()); + writer.append(" "); + writer.append(variable.getName()); + writer.append(IvmlKeyWords.LINEFEED); + } + + writer.append("p CNF " + variableDeclarations.size() + " " + constraints.size()); + writer.append(IvmlKeyWords.LINEFEED); + + for (Constraint constraint : constraints) { + ConstraintSyntaxTree tree = constraint.getConsSyntax(); + writeTree(tree); + } + + writer.flush(); + } + + /** + * Writes the {@link ConstraintSyntaxTree} in the DIMACS format. + * Assumes that the {@link ConstraintSyntaxTree} is in CNF. + * @param tree The {@link ConstraintSyntaxTree} to be written. + * @throws IOException When writing to the {@link Writer} fails + */ + private void writeTree(ConstraintSyntaxTree tree) throws IOException { + + } + + @Override + public void write(String comment, String version) { + try { + if (comment != null) { + writer.append("c "); + writer.append(comment); + writer.append(IvmlKeyWords.LINEFEED); + } + if (version != null) { + writer.append("c Version "); + writer.append(version); + writer.append(IvmlKeyWords.LINEFEED); + } + write(); + } catch (IOException e) { + LOGGER.exception(e); + } + } + + /*DeclarationFinder declarationFinder = new DeclarationFinder(project, FilterType.ALL, null); List variableDeclarations = declarationFinder.getVariableDeclarations(VisibilityType.ALL); Collections.sort(variableDeclarations, new Comparator() { @@ -106,6 +186,5 @@ //out.println(); } - out.flush(); - } + out.flush();*/ } Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/AllTests.java =================================================================== --- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/AllTests.java (revision 59) +++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/AllTests.java (revision 60) @@ -8,4 +8,5 @@ import de.uni_hildesheim.sse.trans.convert.DisjunctionCheckerTest; +import de.uni_hildesheim.sse.trans.convert.MaxTermConverterTest; import de.uni_hildesheim.sse.trans.in.ModelReaderTest; @@ -17,5 +18,5 @@ */ @RunWith(Suite.class) -@SuiteClasses({ ModelReaderTest.class, DisjunctionCheckerTest.class }) +@SuiteClasses({ ModelReaderTest.class, DisjunctionCheckerTest.class, MaxTermConverterTest.class }) public class AllTests { Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java =================================================================== --- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java (revision 60) +++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java (revision 60) @@ -0,0 +1,72 @@ +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.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 MaxTermConverter}. + * + * @author Adam Krafczyk + */ +public class MaxTermConverterTest { + + /** + * 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 MaxTermConverter().convert(constraint); + + ConstraintFinder finder = new ConstraintFinder(testProject); + /*DebugConstraintTreeVisitor visitor = new DebugConstraintTreeVisitor(System.out); + for (Constraint c : finder.getConstraints()) { + c.getConsSyntax().accept(visitor); + }*/ + Assert.assertEquals(4, finder.getConstraints().size()); + } + +} Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/in/ModelReaderTest.java =================================================================== --- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/in/ModelReaderTest.java (revision 59) +++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/in/ModelReaderTest.java (revision 60) @@ -40,8 +40,8 @@ Project project = reader.read(); - PrintStream writer = new PrintStream(new WriterOutputStream(sWriter)); - new DimacsWriter(project).write(writer); + //PrintStream writer = new PrintStream(new WriterOutputStream(sWriter)); + //new DimacsWriter(project).write(System.out); - System.out.println(sWriter); + //System.out.println(sWriter); //project.accept(iWriter);