Index: /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTExpander.java =================================================================== --- /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTExpander.java (revision 427) +++ /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTExpander.java (revision 427) @@ -0,0 +1,302 @@ +package de.uni_hildesheim.sse.trans.convert; + +import de.uni_hildesheim.sse.model.cst.Comment; +import de.uni_hildesheim.sse.model.cst.CompoundAccess; +import de.uni_hildesheim.sse.model.cst.CompoundInitializer; +import de.uni_hildesheim.sse.model.cst.ConstantValue; +import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree; +import de.uni_hildesheim.sse.model.cst.ContainerInitializer; +import de.uni_hildesheim.sse.model.cst.ContainerOperationCall; +import de.uni_hildesheim.sse.model.cst.IConstraintTreeVisitor; +import de.uni_hildesheim.sse.model.cst.IfThen; +import de.uni_hildesheim.sse.model.cst.Let; +import de.uni_hildesheim.sse.model.cst.OCLFeatureCall; +import de.uni_hildesheim.sse.model.cst.Parenthesis; +import de.uni_hildesheim.sse.model.cst.UnresolvedExpression; +import de.uni_hildesheim.sse.model.cst.Variable; +import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords; +import de.uni_hildesheim.sse.model.varModel.filter.DeclrationInConstraintFinder; + +/** + * Tries to simplify a {@link ConstraintSyntaxTree} by expanding a OR (b AND c) + * to (a OR b) AND (a OR c). + * Only works properly if the {@link ConstraintSyntaxTree} only contains AND, + * OR and NOT. First call accept(), then getResult() to get the result. + * + * @author Adam Krafczyk + */ +class CSTExpander implements IConstraintTreeVisitor { + +// private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(CSTSimplifier.class, Main.ID); + + private int minLength; + + private boolean expand; + + private String previousOperation; + + private ConstraintSyntaxTree result; + + /** + * Creates a {@link CSTSimplifier}. + * + * @param minLength The minimum length of a treepart to expand. + */ + public CSTExpander(int minLength) { + this.minLength = minLength; + } + +// /** +// * Getter for the {@link ConstraintSyntaxTree}s created after an accept call. +// * If empty then no simplification of the tree could be found. +// * @return An unmodifiable list of {@link ConstraintSyntaxTree}s, to be +// * interpreted as AND'd together, representing the +// * {@link ConstraintSyntaxTree} that accept()'d this visitor. +// */ +// public List getTrees() { +// return Collections.unmodifiableList(trees); +// } + + /** + * Getter for the {@link ConstraintSyntaxTree}s created after an accept call. + * If null then no simplification of the tree could be found. + * @return The modified {@link ConstraintSyntaxTree}. + */ + public ConstraintSyntaxTree getResult() { + return result; + } + + /** + * Clears the result to reuse the same expander several times. + */ + public void clearResult() { + result = null; + } + + /** + * Returns the "length" of a {@link ConstraintSyntaxTree}. + * @param cst The {@link ConstraintSyntaxTree} to get the "length" of. + * @return The "length" (i.e. the number of variables in the {@link ConstraintSyntaxTree}). + */ + private int getSyntaxTreeLength(ConstraintSyntaxTree cst) { + return new DeclrationInConstraintFinder(cst).getDeclarations().size(); + } + + @Override + public void visitConstantValue(ConstantValue value) {} + + @Override + public void visitVariable(Variable variable) {} + + @Override + public void visitParenthesis(Parenthesis parenthesis) {} + + @Override + public void visitComment(Comment comment) {} + + @Override + public void visitOclFeatureCall(OCLFeatureCall call) { + String currentOperation = call.getOperation(); + if (currentOperation.equals(OclKeyWords.AND) + && previousOperation != null + && previousOperation.equals(OclKeyWords.OR)) { + + expand = true; + return; // don't fall into the if block below + + } else { + boolean left = true; + + previousOperation = call.getOperation(); + if (getSyntaxTreeLength(call.getOperand()) >= minLength) { + call.getOperand().accept(this); + } + + left = false; + + if (currentOperation.equals(OclKeyWords.OR) + || currentOperation.equals(OclKeyWords.AND)) { + previousOperation = call.getOperation(); + if (getSyntaxTreeLength(call.getParameter(0)) >= minLength) { + call.getParameter(0).accept(this); + } + } + + if (expand) { + ConstraintSyntaxTree a; + ConstraintSyntaxTree b; + ConstraintSyntaxTree c; + if (left) { + // "call" is currently an OR with an AND at the left: + // (b AND c) OR a + a = call.getParameter(0); + OCLFeatureCall andCall = (OCLFeatureCall) call.getOperand(); + b = andCall.getOperand(); + c = andCall.getParameter(0); + + } else { + // "call" is currently an OR with an AND at the right: + // a OR (b AND c) + a = call.getOperand(); + OCLFeatureCall andCall = (OCLFeatureCall) call.getParameter(0); + b = andCall.getOperand(); + c = andCall.getParameter(0); + } + // construct the new call + OCLFeatureCall newLeft = new OCLFeatureCall(a, OclKeyWords.OR, b); + OCLFeatureCall newRight = new OCLFeatureCall(a, OclKeyWords.OR, c); + result = new OCLFeatureCall(newLeft, OclKeyWords.AND, newRight); + } + } + } +// switch (state) { +// case INITIAL: +// if (call.getOperation().equals(OclKeyWords.OR)) { +// LOGGER.info("Highest operation is an OR"); +// +// state = State.EXPAND; +// +// call.getOperand().accept(this); +// ConstraintSyntaxTree passedOperand = passUp; +// passUp = null; +// +// if (leftTree != null && rightTree != null) { +// trees.add(new OCLFeatureCall(leftTree, OclKeyWords.OR, call.getParameter(0))); +// trees.add(new OCLFeatureCall(rightTree, OclKeyWords.OR, call.getParameter(0))); +// } else { +// +// call.getParameter(0).accept(this); +// ConstraintSyntaxTree passedParameter = passUp; +// passUp = null; +// +// if (leftTree != null && rightTree != null) { +// trees.add(new OCLFeatureCall(leftTree, OclKeyWords.OR, call.getOperand())); +// trees.add(new OCLFeatureCall(rightTree, OclKeyWords.OR, +// call.getOperand())); +// } +// +// if (passedOperand != null) { +// if (passedParameter != null) { +// trees.add(new OCLFeatureCall(passedOperand, OclKeyWords.OR, passedParameter)); +// } else { +// trees.add(new OCLFeatureCall(passedOperand, OclKeyWords.OR, call.getParameter(0))); +// } +// } else { +// if (passedParameter != null) { +// trees.add(new OCLFeatureCall(call.getOperand(), OclKeyWords.OR, passedParameter)); +// } +// } +// } +// +// state = State.INITIAL; +// +// } else if (call.getOperation().equals(OclKeyWords.AND)) { +// LOGGER.info("Highest operation is an AND"); +// // split tree +// trees.add(call.getOperand()); +// trees.add(call.getParameter(0)); +// } +// break; +// +// case EXPAND: // highest operand is an OR +// if (call.getOperation().equals(OclKeyWords.AND)) { +// LOGGER.info("Second highest operation is an AND"); +// +// leftTree = call.getOperand(); +// rightTree = call.getParameter(0); +// } else if (call.getOperation().equals(OclKeyWords.NOT)) { +// LOGGER.info("Second highest operation is a NOT"); +// +// state = State.NEGATE_EXPAND; +// +// call.getOperand().accept(this); +// +// state = State.EXPAND; +// } +// break; +// +// case NEGATE_EXPAND: // highest operand is an OR; second highest is a NOT +// // if this operation is an OR then expand the NOT into it +// if (call.getOperation().equals(OclKeyWords.OR)) { +// LOGGER.info("Third highest (negated) operation is an OR"); +// leftTree = new OCLFeatureCall(call.getOperand(), OclKeyWords.NOT); +// rightTree = new OCLFeatureCall(call.getParameter(0), OclKeyWords.NOT); +// break; +// } +// state = State.NEGATE; +// +// // fall through +// case NEGATE: // some level below a NOT +// // recursively expand the not further down into the tree +// +// if (call.getOperation().equals(OclKeyWords.AND)) { +// LOGGER.info("Negating an AND"); +// +// call.getOperand().accept(this); +// ConstraintSyntaxTree leftSide = passUp; +// passUp = null; +// if (leftSide == null) { +// leftSide = new OCLFeatureCall(call.getOperand(), OclKeyWords.NOT); +// } +// +// call.getParameter(0).accept(this); +// ConstraintSyntaxTree rightSide = passUp; +// passUp = null; +// if (rightSide == null) { +// rightSide = new OCLFeatureCall(call.getParameter(0), OclKeyWords.NOT); +// } +// +// passUp = new OCLFeatureCall(leftSide, OclKeyWords.OR, rightSide); +// +// } else if (call.getOperation().equals(OclKeyWords.OR)) { +// LOGGER.info("Negating an OR"); +// +// call.getOperand().accept(this); +// ConstraintSyntaxTree leftSide = passUp; +// passUp = null; +// if (leftSide == null) { +// leftSide = new OCLFeatureCall(call.getOperand(), OclKeyWords.NOT); +// } +// +// call.getParameter(0).accept(this); +// ConstraintSyntaxTree rightSide = passUp; +// passUp = null; +// if (rightSide == null) { +// rightSide = new OCLFeatureCall(call.getParameter(0), OclKeyWords.NOT); +// } +// +// passUp = new OCLFeatureCall(leftSide, OclKeyWords.AND, rightSide); +// +// } else if (call.getOperation().equals(OclKeyWords.NOT)) { +// LOGGER.info("Negating a NOT"); +// +// passUp = call.getOperand(); +// } +// break; +// +// default: +// break; +// } + + @Override + public void visitLet(Let let) {} + + @Override + public void visitIfThen(IfThen ifThen) {} + + @Override + public void visitContainerOperationCall(ContainerOperationCall call) {} + + @Override + public void visitCompoundAccess(CompoundAccess access) {} + + @Override + public void visitUnresolvedExpression(UnresolvedExpression expression) {} + + @Override + public void visitCompoundInitializer(CompoundInitializer initializer) {} + + @Override + public void visitContainerInitializer(ContainerInitializer initializer) {} + +} Index: /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTNegater.java =================================================================== --- /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTNegater.java (revision 427) +++ /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTNegater.java (revision 427) @@ -0,0 +1,141 @@ +package de.uni_hildesheim.sse.trans.convert; + +import de.uni_hildesheim.sse.model.cst.Comment; +import de.uni_hildesheim.sse.model.cst.CompoundAccess; +import de.uni_hildesheim.sse.model.cst.CompoundInitializer; +import de.uni_hildesheim.sse.model.cst.ConstantValue; +import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree; +import de.uni_hildesheim.sse.model.cst.ContainerInitializer; +import de.uni_hildesheim.sse.model.cst.ContainerOperationCall; +import de.uni_hildesheim.sse.model.cst.IConstraintTreeVisitor; +import de.uni_hildesheim.sse.model.cst.IfThen; +import de.uni_hildesheim.sse.model.cst.Let; +import de.uni_hildesheim.sse.model.cst.OCLFeatureCall; +import de.uni_hildesheim.sse.model.cst.Parenthesis; +import de.uni_hildesheim.sse.model.cst.UnresolvedExpression; +import de.uni_hildesheim.sse.model.cst.Variable; +import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords; + +/** + * Moves negations further into the {@link ConstraintSyntaxTree}. + * I.e. !(a OR b) will be converted to (!a AND !b). + * First call accept(), then getResult() to get the result. + * + * @author Adam Krafczyk + */ +class CSTNegater implements IConstraintTreeVisitor { + + private ConstraintSyntaxTree result; + private boolean negated = false; + + /** + * Getter for the result after an accept() call. + * @return The modified {@link ConstraintSyntaxTree}. + */ + public ConstraintSyntaxTree getResult() { + return result; + } + + @Override + public void visitConstantValue(ConstantValue value) { + throw new RuntimeException("Unexpected CST"); // TODO; + } + + @Override + public void visitVariable(Variable variable) { + if (negated) { + result = new OCLFeatureCall(variable, OclKeyWords.NOT); + } else { + result = variable; + } + } + + @Override + public void visitParenthesis(Parenthesis parenthesis) { + parenthesis.getExpr().accept(this); + } + + @Override + public void visitComment(Comment comment) { + throw new RuntimeException("Unexpected CST"); // TODO; + } + + @Override + public void visitOclFeatureCall(OCLFeatureCall call) { + switch (call.getOperation()) { + case OclKeyWords.OR: + case OclKeyWords.AND: + boolean currentNegated = negated; + + result = null; + call.getOperand().accept(this); + negated = currentNegated; + ConstraintSyntaxTree leftSide = getResult(); + + result = null; + call.getParameter(0).accept(this); + negated = currentNegated; + ConstraintSyntaxTree rightSide = getResult(); + + String operation = call.getOperation(); + + if (negated) { + if (call.getOperation().equals(OclKeyWords.AND)) { + operation = OclKeyWords.OR; + } else { + operation = OclKeyWords.AND; + } + } + + result = new OCLFeatureCall(leftSide, operation, rightSide); + break; + + case OclKeyWords.NOT: + negated = !negated; + call.getOperand().accept(this); + + // result = result; + + break; + + default: + throw new RuntimeException("Unexpected operation"); // TODO; + } + } + + @Override + public void visitLet(Let let) { + throw new RuntimeException("Unexpected CST"); // TODO; + } + + @Override + public void visitIfThen(IfThen ifThen) { + throw new RuntimeException("Unexpected CST"); // TODO; + } + + @Override + public void visitContainerOperationCall(ContainerOperationCall call) { + throw new RuntimeException("Unexpected CST"); // TODO; + } + + @Override + public void visitCompoundAccess(CompoundAccess access) { + throw new RuntimeException("Unexpected CST"); // TODO; + } + + @Override + public void visitUnresolvedExpression(UnresolvedExpression expression) { + throw new RuntimeException("Unexpected CST"); // TODO; + } + + @Override + public void visitCompoundInitializer(CompoundInitializer initializer) { + throw new RuntimeException("Unexpected CST"); // TODO; + } + + @Override + public void visitContainerInitializer(ContainerInitializer initializer) { + throw new RuntimeException("Unexpected CST"); // TODO; + } + +} Index: delTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTSimplifier.java =================================================================== --- /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/CSTSimplifier.java (revision 426) +++ (revision ) @@ -1,268 +1,0 @@ -package de.uni_hildesheim.sse.trans.convert; - -import java.util.ArrayList; -import java.util.Collections; -import java.util.List; - -import de.uni_hildesheim.sse.model.cst.Comment; -import de.uni_hildesheim.sse.model.cst.CompoundAccess; -import de.uni_hildesheim.sse.model.cst.CompoundInitializer; -import de.uni_hildesheim.sse.model.cst.ConstantValue; -import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree; -import de.uni_hildesheim.sse.model.cst.ContainerInitializer; -import de.uni_hildesheim.sse.model.cst.ContainerOperationCall; -import de.uni_hildesheim.sse.model.cst.IConstraintTreeVisitor; -import de.uni_hildesheim.sse.model.cst.IfThen; -import de.uni_hildesheim.sse.model.cst.Let; -import de.uni_hildesheim.sse.model.cst.OCLFeatureCall; -import de.uni_hildesheim.sse.model.cst.Parenthesis; -import de.uni_hildesheim.sse.model.cst.UnresolvedExpression; -import de.uni_hildesheim.sse.model.cst.Variable; -import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords; -import de.uni_hildesheim.sse.model.varModel.filter.DeclrationInConstraintFinder; - -/** - * Tries to simplify a {@link ConstraintSyntaxTree} by expanding a OR (b AND c) - * to (a OR b) AND (a OR c). - * Only works properly if the {@link ConstraintSyntaxTree} only contains AND, - * OR and NOT. First call accept(), then getTrees() to get the result. - * - * @author Adam Krafczyk - */ -class CSTSimplifier implements IConstraintTreeVisitor { - -// private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(CSTSimplifier.class, Main.ID); - - private static final int MIN_LENGTH = 14; - - /** - * Possible states of the visitor. - */ - private enum State { - FIND_POSSIBLE_EXPANSION, - } - private State state = State.FIND_POSSIBLE_EXPANSION; - - private String previousOperation; - - private List trees; - - /** - * Creates a {@link CSTSimplifier}. - */ - public CSTSimplifier() { - trees = new ArrayList(); - } - - /** - * Getter for the {@link ConstraintSyntaxTree}s created after an accept call. - * @return An unmodifiable list of {@link ConstraintSyntaxTree}s, to be - * interpreted as AND'd together, representing the - * {@link ConstraintSyntaxTree} that accept()'d this visitor. - */ - public List getTrees() { - return Collections.unmodifiableList(trees); - } - - /** - * Returns the "length" of a {@link ConstraintSyntaxTree}. - * @param cst The {@link ConstraintSyntaxTree} to get the "length" of. - * @return The "length" (i.e. the number of variables in the {@link ConstraintSyntaxTree}). - */ - private int getSyntaxTreeLength(ConstraintSyntaxTree cst) { - return new DeclrationInConstraintFinder(cst).getDeclarations().size(); - } - - @Override - public void visitConstantValue(ConstantValue value) {} - - @Override - public void visitVariable(Variable variable) {} - - @Override - public void visitParenthesis(Parenthesis parenthesis) {} - - @Override - public void visitComment(Comment comment) {} - - @Override - public void visitOclFeatureCall(OCLFeatureCall call) { - switch (state) { - case FIND_POSSIBLE_EXPANSION: - String currentOperation = call.getOperation(); - if (currentOperation.equals(OclKeyWords.AND) - && previousOperation.equals(OclKeyWords.OR)) { - - // TODO expand - - } else { - previousOperation = call.getOperation(); - if (getSyntaxTreeLength(call.getOperand()) >= MIN_LENGTH) { - call.getOperand().accept(this); - } - - if (currentOperation.equals(OclKeyWords.OR) - || currentOperation.equals(OclKeyWords.AND)) { - previousOperation = call.getOperation(); - if (getSyntaxTreeLength(call.getParameter(0)) >= MIN_LENGTH) { - call.getParameter(0).accept(this); - } - } - } - break; - - default: - break; - } -// switch (state) { -// case INITIAL: -// if (call.getOperation().equals(OclKeyWords.OR)) { -// LOGGER.info("Highest operation is an OR"); -// -// state = State.EXPAND; -// -// call.getOperand().accept(this); -// ConstraintSyntaxTree passedOperand = passUp; -// passUp = null; -// -// if (leftTree != null && rightTree != null) { -// trees.add(new OCLFeatureCall(leftTree, OclKeyWords.OR, call.getParameter(0))); -// trees.add(new OCLFeatureCall(rightTree, OclKeyWords.OR, call.getParameter(0))); -// } else { -// -// call.getParameter(0).accept(this); -// ConstraintSyntaxTree passedParameter = passUp; -// passUp = null; -// -// if (leftTree != null && rightTree != null) { -// trees.add(new OCLFeatureCall(leftTree, OclKeyWords.OR, call.getOperand())); -// trees.add(new OCLFeatureCall(rightTree, OclKeyWords.OR, -// call.getOperand())); -// } -// -// if (passedOperand != null) { -// if (passedParameter != null) { -// trees.add(new OCLFeatureCall(passedOperand, OclKeyWords.OR, passedParameter)); -// } else { -// trees.add(new OCLFeatureCall(passedOperand, OclKeyWords.OR, call.getParameter(0))); -// } -// } else { -// if (passedParameter != null) { -// trees.add(new OCLFeatureCall(call.getOperand(), OclKeyWords.OR, passedParameter)); -// } -// } -// } -// -// state = State.INITIAL; -// -// } else if (call.getOperation().equals(OclKeyWords.AND)) { -// LOGGER.info("Highest operation is an AND"); -// // split tree -// trees.add(call.getOperand()); -// trees.add(call.getParameter(0)); -// } -// break; -// -// case EXPAND: // highest operand is an OR -// if (call.getOperation().equals(OclKeyWords.AND)) { -// LOGGER.info("Second highest operation is an AND"); -// -// leftTree = call.getOperand(); -// rightTree = call.getParameter(0); -// } else if (call.getOperation().equals(OclKeyWords.NOT)) { -// LOGGER.info("Second highest operation is a NOT"); -// -// state = State.NEGATE_EXPAND; -// -// call.getOperand().accept(this); -// -// state = State.EXPAND; -// } -// break; -// -// case NEGATE_EXPAND: // highest operand is an OR; second highest is a NOT -// // if this operation is an OR then expand the NOT into it -// if (call.getOperation().equals(OclKeyWords.OR)) { -// LOGGER.info("Third highest (negated) operation is an OR"); -// leftTree = new OCLFeatureCall(call.getOperand(), OclKeyWords.NOT); -// rightTree = new OCLFeatureCall(call.getParameter(0), OclKeyWords.NOT); -// break; -// } -// state = State.NEGATE; -// -// // fall through -// case NEGATE: // some level below a NOT -// // recursively expand the not further down into the tree -// -// if (call.getOperation().equals(OclKeyWords.AND)) { -// LOGGER.info("Negating an AND"); -// -// call.getOperand().accept(this); -// ConstraintSyntaxTree leftSide = passUp; -// passUp = null; -// if (leftSide == null) { -// leftSide = new OCLFeatureCall(call.getOperand(), OclKeyWords.NOT); -// } -// -// call.getParameter(0).accept(this); -// ConstraintSyntaxTree rightSide = passUp; -// passUp = null; -// if (rightSide == null) { -// rightSide = new OCLFeatureCall(call.getParameter(0), OclKeyWords.NOT); -// } -// -// passUp = new OCLFeatureCall(leftSide, OclKeyWords.OR, rightSide); -// -// } else if (call.getOperation().equals(OclKeyWords.OR)) { -// LOGGER.info("Negating an OR"); -// -// call.getOperand().accept(this); -// ConstraintSyntaxTree leftSide = passUp; -// passUp = null; -// if (leftSide == null) { -// leftSide = new OCLFeatureCall(call.getOperand(), OclKeyWords.NOT); -// } -// -// call.getParameter(0).accept(this); -// ConstraintSyntaxTree rightSide = passUp; -// passUp = null; -// if (rightSide == null) { -// rightSide = new OCLFeatureCall(call.getParameter(0), OclKeyWords.NOT); -// } -// -// passUp = new OCLFeatureCall(leftSide, OclKeyWords.AND, rightSide); -// -// } else if (call.getOperation().equals(OclKeyWords.NOT)) { -// LOGGER.info("Negating a NOT"); -// -// passUp = call.getOperand(); -// } -// break; -// -// default: -// break; -// } - } - - @Override - public void visitLet(Let let) {} - - @Override - public void visitIfThen(IfThen ifThen) {} - - @Override - public void visitContainerOperationCall(ContainerOperationCall call) {} - - @Override - public void visitCompoundAccess(CompoundAccess access) {} - - @Override - public void visitUnresolvedExpression(UnresolvedExpression expression) {} - - @Override - public void visitCompoundInitializer(CompoundInitializer initializer) {} - - @Override - public void visitContainerInitializer(ContainerInitializer initializer) {} - -} Index: /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java =================================================================== --- /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 426) +++ /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java (revision 427) @@ -5,5 +5,4 @@ import java.util.Comparator; import java.util.HashMap; -import java.util.List; import java.util.Map; import java.util.Set; @@ -15,5 +14,4 @@ import de.uni_hildesheim.sse.model.cst.CSTSemanticException; import de.uni_hildesheim.sse.model.cst.ConstraintSyntaxTree; -import de.uni_hildesheim.sse.model.cst.DebugConstraintTreeVisitor; import de.uni_hildesheim.sse.model.cst.OCLFeatureCall; import de.uni_hildesheim.sse.model.cst.Parenthesis; @@ -42,4 +40,6 @@ private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(MaxTermConverter.class, Main.ID); + private static final int MIN_SIMPLYIFY_LENGTH = 18; + private Project project; private Map variablesCache = new HashMap(); @@ -70,4 +70,13 @@ /** + * Returns the "length" of a {@link ConstraintSyntaxTree}. + * @param cst The {@link ConstraintSyntaxTree} to get the "length" of. + * @return The "length" (i.e. the number of variables in the {@link ConstraintSyntaxTree}). + */ + private int getSyntaxTreeLength(ConstraintSyntaxTree cst) { + return new DeclrationInConstraintFinder(cst).getDeclarations().size(); + } + + /** * Converts the given expression into CNF and adds it via * {@link MaxTermConverter#addConstraint(ConstraintSyntaxTree)}. @@ -83,5 +92,26 @@ } -// originalConstraint.accept(new DebugConstraintTreeVisitor()); + if (getSyntaxTreeLength(originalConstraint) >= MIN_SIMPLYIFY_LENGTH) { + LOGGER.info("Constraint is longer than " + MIN_SIMPLYIFY_LENGTH + ", trying to simplify"); + + // pull in NOT's as far as possible + CSTNegater negater = new CSTNegater(); + originalConstraint.accept(negater); + originalConstraint = negater.getResult(); + + // expand to get closer to CNF + CSTExpander expander = new CSTExpander(MIN_SIMPLYIFY_LENGTH); + int numExpanded = 0; + do { + expander.clearResult(); + originalConstraint.accept(expander); + if (expander.getResult() != null) { + originalConstraint = expander.getResult(); + numExpanded++; + } + } while (expander.getResult() != null); + + LOGGER.info("Found " + numExpanded + " possible expansions to simplify constraint"); + } // Split top level AND calls into two separate terms @@ -89,5 +119,5 @@ OCLFeatureCall call = (OCLFeatureCall) originalConstraint; if (call.getOperation().equals(OclKeyWords.AND)) { - LOGGER.info("highest operation is an AND"); + LOGGER.info("Highest operation is an AND, splitting"); createCNFParts(call.getOperand()); createCNFParts(call.getParameter(0)); @@ -97,145 +127,5 @@ if (!handled) { - CSTSimplifier simplifier = new CSTSimplifier(); - originalConstraint.accept(simplifier); - List trees = simplifier.getTrees(); - if (trees.size() > 0) { - LOGGER.info("Optimized tree"); - for (ConstraintSyntaxTree tree : trees) { - createCNFParts(tree); - } - handled = true; - } - } - -// -// // Handle an OR with an AND at one side -// if (!handled && originalConstraint instanceof OCLFeatureCall) { -// OCLFeatureCall highestOperation = (OCLFeatureCall) originalConstraint; -// -// // if highest operation is an OR -// if (highestOperation.getOperation().equals(OclKeyWords.OR)) { -// LOGGER.info("highest operation is an OR"); -// if (highestOperation.getOperand() instanceof OCLFeatureCall) { -// OCLFeatureCall leftOperation = (OCLFeatureCall) highestOperation.getOperand(); -// -// // if the left side of the OR is an AND -// if (leftOperation.getOperation().equals(OclKeyWords.AND)) { -// LOGGER.info("left side is an and"); -// OCLFeatureCall call1 = new OCLFeatureCall(leftOperation.getOperand(), -// OclKeyWords.OR, highestOperation.getParameter(0)); -// OCLFeatureCall call2 = new OCLFeatureCall(leftOperation.getParameter(0), -// OclKeyWords.OR, highestOperation.getParameter(0)); -// -// createCNFParts(call1); -// createCNFParts(call2); -// handled = true; -// } -// -// // if the left side of the OR is a NOT -// if (!handled && leftOperation.getOperation().equals(OclKeyWords.NOT)) { -// LOGGER.info("left side is a NOT"); -// if (leftOperation.getOperand() instanceof OCLFeatureCall) { -// OCLFeatureCall negatedOperation = (OCLFeatureCall) leftOperation.getOperand(); -// -// // if the operation inside the NOT is an AND -// if (negatedOperation.getOperation().equals(OclKeyWords.AND)) { -// LOGGER.info("negated operation is an AND"); -// -// // expand the NOT into the and call -// OCLFeatureCall newOperand2 = new OCLFeatureCall( -// new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), -// OclKeyWords.OR, -// new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); -// -// OCLFeatureCall newCall = new OCLFeatureCall(newOperand2, -// OclKeyWords.OR, highestOperation.getParameter(0)); -// createCNFParts(newCall); -// handled = true; -// } -// -// // if the operation inside the NOT is an OR -// if (negatedOperation.getOperation().equals(OclKeyWords.OR)) { -// LOGGER.info("negated operation is an OR"); -// -// // expand the NOT into the and call -// OCLFeatureCall newOperand2 = new OCLFeatureCall( -// new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), -// OclKeyWords.AND, -// new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); -// -// OCLFeatureCall newCall = new OCLFeatureCall(newOperand2, -// OclKeyWords.OR, highestOperation.getParameter(0)); -// createCNFParts(newCall); -// handled = true; -// } -// } -// } -// } -// -// if (!handled && highestOperation.getParameter(0) instanceof OCLFeatureCall) { -// OCLFeatureCall rightSide = (OCLFeatureCall) highestOperation.getParameter(0); -// -// // if the right side of the call is an AND -// if (rightSide.getOperation().equals(OclKeyWords.AND)) { -// LOGGER.info("right side is an AND"); -// OCLFeatureCall call1 = new OCLFeatureCall(rightSide.getOperand(), -// OclKeyWords.OR, highestOperation.getOperand()); -// OCLFeatureCall call2 = new OCLFeatureCall(rightSide.getParameter(0), -// OclKeyWords.OR, highestOperation.getOperand()); -// -// createCNFParts(call1); -// createCNFParts(call2); -// handled = true; -// } -// -// // if the right side of the OR is a NOT -// if (!handled && rightSide.getOperation().equals(OclKeyWords.NOT)) { -// LOGGER.info("right side is a NOT"); -// if (rightSide.getOperand() instanceof OCLFeatureCall) { -// OCLFeatureCall negatedOperation = (OCLFeatureCall) rightSide.getOperand(); -// -// // if the operation inside the NOT is an AND -// if (negatedOperation.getOperation().equals(OclKeyWords.AND)) { -// LOGGER.info("negated operation is an AND"); -// -// // expand the NOT into the and call -// OCLFeatureCall newOperand2 = new OCLFeatureCall( -// new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), -// OclKeyWords.OR, -// new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); -// -// OCLFeatureCall newCall = new OCLFeatureCall(newOperand2, -// OclKeyWords.OR, highestOperation.getOperand()); -// createCNFParts(newCall); -// handled = true; -// } -// -// // if the operation inside the NOT is an OR -// if (negatedOperation.getOperation().equals(OclKeyWords.OR)) { -// LOGGER.info("negated operation is an OR"); -// -// // expand the NOT into the and call -// OCLFeatureCall newOperand2 = new OCLFeatureCall( -// new OCLFeatureCall(negatedOperation.getOperand(), OclKeyWords.NOT), -// OclKeyWords.AND, -// new OCLFeatureCall(negatedOperation.getParameter(0), OclKeyWords.NOT)); -// -// OCLFeatureCall newCall = new OCLFeatureCall(highestOperation.getOperand(), -// OclKeyWords.OR, newOperand2); -// createCNFParts(newCall); -// handled = true; -// } -// } -// } -// } -// -// } -// } - - if (!handled) { // Stop recursion! - -// originalConstraint.accept(new DebugConstraintTreeVisitor()); // Get an array of all variables in the constraint Index: /ModelTranslator/test/de/uni_hildesheim/sse/trans/AllTests.java =================================================================== --- /ModelTranslator/test/de/uni_hildesheim/sse/trans/AllTests.java (revision 426) +++ /ModelTranslator/test/de/uni_hildesheim/sse/trans/AllTests.java (revision 427) @@ -9,4 +9,6 @@ import org.junit.runners.Suite.SuiteClasses; +import de.uni_hildesheim.sse.trans.convert.CSTNegaterTest; +import de.uni_hildesheim.sse.trans.convert.CSTExpanderTest; import de.uni_hildesheim.sse.trans.convert.DisjunctionCheckerTest; import de.uni_hildesheim.sse.trans.convert.LiteralFinderTest; @@ -35,5 +37,7 @@ DimacsWriterTest.class, LiteralFinderTest.class, - RsfToDimacsTranslationTest.class + RsfToDimacsTranslationTest.class, + CSTNegaterTest.class, + CSTExpanderTest.class }) public class AllTests { Index: /ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/CSTExpanderTest.java =================================================================== --- /ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/CSTExpanderTest.java (revision 427) +++ /ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/CSTExpanderTest.java (revision 427) @@ -0,0 +1,65 @@ +package de.uni_hildesheim.sse.trans.convert; + +import junit.framework.Assert; + +import org.junit.Test; + +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.varModel.DecisionVariableDeclaration; +import de.uni_hildesheim.sse.model.varModel.datatypes.BooleanType; +import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords; + +/** + * Tests the {@link CSTExpander} class. + * + * @author Adam Krafczyk + */ +public class CSTExpanderTest { + + /** + * Tests the {@link CSTExpander}. + */ + @Test + public void testCSTSimplifier() { + 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 varA = new Variable(declA); + Variable varB = new Variable(declB); + Variable varC = new Variable(declC); + + // create: a OR (b AND c) + OCLFeatureCall call = new OCLFeatureCall(varB, OclKeyWords.AND, varC); + call = new OCLFeatureCall(varA, OclKeyWords.OR, call); + + CSTExpander expander = new CSTExpander(0); + call.accept(expander); + + // result should be: (a OR b) AND (a OR c) + ConstraintSyntaxTree result = expander.getResult(); + + Assert.assertTrue(result instanceof OCLFeatureCall); + + OCLFeatureCall resultCall = (OCLFeatureCall) result; + Assert.assertEquals(OclKeyWords.AND, resultCall.getOperation()); + + Assert.assertTrue(resultCall.getOperand() instanceof OCLFeatureCall); + Assert.assertTrue(resultCall.getParameter(0) instanceof OCLFeatureCall); + + OCLFeatureCall left = (OCLFeatureCall) resultCall.getOperand(); + OCLFeatureCall right = (OCLFeatureCall) resultCall.getParameter(0); + + Assert.assertEquals(OclKeyWords.OR, left.getOperation()); + Assert.assertEquals(OclKeyWords.OR, right.getOperation()); + + Assert.assertTrue(left.getOperand().equals(varA) || left.getParameter(0).equals(varA)); + Assert.assertTrue(left.getOperand().equals(varB) || left.getParameter(0).equals(varB)); + + Assert.assertTrue(right.getOperand().equals(varA) || right.getParameter(0).equals(varA)); + Assert.assertTrue(right.getOperand().equals(varC) || right.getParameter(0).equals(varC)); + } + +} Index: /ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/CSTNegaterTest.java =================================================================== --- /ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/CSTNegaterTest.java (revision 427) +++ /ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/CSTNegaterTest.java (revision 427) @@ -0,0 +1,68 @@ +package de.uni_hildesheim.sse.trans.convert; + +import junit.framework.Assert; + +import org.junit.Test; + +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.varModel.DecisionVariableDeclaration; +import de.uni_hildesheim.sse.model.varModel.datatypes.BooleanType; +import de.uni_hildesheim.sse.model.varModel.datatypes.OclKeyWords; + +/** + * Tests the {@link CSTNegater} class. + * + * @author Adam Krafczyk + */ +public class CSTNegaterTest { + + /** + * Tests the {@link CSTNegater}. + */ + @Test + public void testCSTNegater() { + 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 varA = new Variable(declA); + Variable varB = new Variable(declB); + Variable varC = new Variable(declC); + + // create: !(a OR (b AND !c)) + OCLFeatureCall call = new OCLFeatureCall(varC, OclKeyWords.NOT); + call = new OCLFeatureCall(varB, OclKeyWords.AND, call); + call = new OCLFeatureCall(varA, OclKeyWords.OR, call); + call = new OCLFeatureCall(call, OclKeyWords.NOT); + + CSTNegater negater = new CSTNegater(); + call.accept(negater); + + // result should be: !a AND (!b OR c) + ConstraintSyntaxTree result = negater.getResult(); + + Assert.assertTrue(result instanceof OCLFeatureCall); + + OCLFeatureCall resultCall = (OCLFeatureCall) result; + Assert.assertEquals(OclKeyWords.AND, resultCall.getOperation()); + + Assert.assertTrue(resultCall.getOperand() instanceof OCLFeatureCall); + Assert.assertEquals(OclKeyWords.NOT, + ((OCLFeatureCall) resultCall.getOperand()).getOperation()); + Assert.assertEquals(varA, + ((OCLFeatureCall) resultCall.getOperand()).getOperand()); + + Assert.assertTrue(resultCall.getParameter(0) instanceof OCLFeatureCall); + resultCall = (OCLFeatureCall) resultCall.getParameter(0); + + Assert.assertEquals(OclKeyWords.OR, resultCall.getOperation()); + Assert.assertEquals(varC, resultCall.getParameter(0)); + + Assert.assertTrue(resultCall.getOperand() instanceof OCLFeatureCall); + Assert.assertEquals(OclKeyWords.NOT, ((OCLFeatureCall) resultCall.getOperand()).getOperation()); + Assert.assertEquals(varB, ((OCLFeatureCall) resultCall.getOperand()).getOperand()); + } + +}