Index: /Code/ModelTranslator/scripts/ivmlExample.sh =================================================================== --- /Code/ModelTranslator/scripts/ivmlExample.sh (revision 117) +++ /Code/ModelTranslator/scripts/ivmlExample.sh (revision 118) @@ -4,5 +4,7 @@ #$ -l mem=10000m #$ -q all.q,fast.q,acogpr.q +#$ -N ModelTranslation +#$ -m abe # # -java -Xms8000m -Xmx8000m -XX:ParallelGCThreads=1 -XX:ConcGCThreads=1 -jar ModelTranslator.jar -in input/model.model output/Linux_x86_2.6.33.3.ivml -v 2.6.33.3 -comment "X86 translation of Linux 2.6.33.3 using KConfigReader" +java -Xms8000m -Xmx8000m -XX:ParallelGCThreads=1 -XX:ConcGCThreads=1 -jar ModelTranslator.jar -in input/Linux.tsv -out output/Linux_x86_2.6.33.3.ivml -v 2.6.33.3 -comment "X86 translation of Linux 2.6.33.3 using KConfigReader" Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java (revision 117) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/ModelTranslator.java (revision 118) @@ -86,35 +86,5 @@ if (optimizations.hasAtLeastOneOption()) { LOGGER.info(step++ + ".) Optimize model."); - boolean optimizationApplied = true; - int run = 1; - - while (optimizationApplied) { - // Initialization - LOGGER.info("Optimization run " + run++); - ModelOptimizer optimizer = new ModelOptimizer(model); - optimizationApplied = false; - int removed = 0; - - // Removing unused variables - if (optimizations.removeUnusedVariables()) { - removed = optimizer.removeUnusedVariables(); - LOGGER.info("Removed " + removed + " unused variables."); - optimizationApplied |= removed > 0; - } - - // Removing constant "variables" - if (optimizations.eleminateConstants()) { - removed = optimizer.handleConstantVariables(); - LOGGER.info("Removed " + removed + " constraints with constant variables."); - optimizationApplied |= removed > 0; - } - - // Duplicated constraints - if (optimizations.removeDuplicatedConstraints()) { - removed = optimizer.removeDuplicatedConstraints(); - LOGGER.info("Removed " + removed + " duplicated constraints."); - optimizationApplied |= removed > 0; - } - } + optimizeModel(model, optimizations); } @@ -138,4 +108,43 @@ } } + + /** + * Optimizes a CNF Model using the {@link ModelOptimizer}. + * @param model A model in CNF form to be optimized. + * @param optimizations A specification which optimizations shall be applied. + */ + private static void optimizeModel(Project model, OptimizationParameter optimizations) { + boolean optimizationApplied = true; + int run = 1; + + while (optimizationApplied) { + // Initialization + LOGGER.info("Optimization run " + run++); + ModelOptimizer optimizer = new ModelOptimizer(model); + optimizationApplied = false; + int removed = 0; + + // Removing unused variables + if (optimizations.removeUnusedVariables()) { + removed = optimizer.removeUnusedVariables(); + LOGGER.info("Removed " + removed + " unused variables."); + optimizationApplied |= removed > 0; + } + + // Removing constant "variables" + if (optimizations.eleminateConstants()) { + removed = optimizer.handleConstantVariables(); + LOGGER.info("Removed " + removed + " constraints with constant variables."); + optimizationApplied |= removed > 0; + } + + // Duplicated constraints + if (optimizations.removeDuplicatedConstraints()) { + removed = optimizer.removeDuplicatedConstraints(); + LOGGER.info("Removed " + removed + " duplicated constraints."); + optimizationApplied |= removed > 0; + } + } + } /** Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ConstraintContainer.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ConstraintContainer.java (revision 118) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ConstraintContainer.java (revision 118) @@ -0,0 +1,41 @@ +package de.uni_hildesheim.sse.trans.convert; + +import java.util.Set; + +import de.uni_hildesheim.sse.model.varModel.Constraint; + +/** + * 2-tuple of (constraint, used literals). + * @author El-Sharkawy + * + */ +class ConstraintContainer { + private Constraint constraint; + private Set literals; + + /** + * Sole constructor. + * @param constraint The constraint to hold + * @param literals the literals (positive/negative declarations) of the related constraint + */ + ConstraintContainer(Constraint constraint, Set literals) { + this.constraint = constraint; + this.literals = literals; + } + + /** + * Getter for the constraint. + * @return The constraint + */ + Constraint getConstraint() { + return constraint; + } + + /** + * Getter for the literals. + * @return The literals (positive/negative declarations) of the related constraint + */ + Set getLiterals() { + return literals; + } +} Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ConstraintMap.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ConstraintMap.java (revision 118) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ConstraintMap.java (revision 118) @@ -0,0 +1,45 @@ +package de.uni_hildesheim.sse.trans.convert; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +/** + * Will store constraints having the same attribute (like the length of the constraint) into a shared list. + * @author El-Sharkawy + * + * @param The attribute defining which constraints shall be stored in a shared list, + * e.g. length of the constraints. + * @param The {@link de.uni_hildesheim.sse.model.varModel.Constraint}s or {@link ConstraintContainer}s. + */ +public class ConstraintMap { + private Map> map = new HashMap>(); + + /** + * Returns the list of constraints for the given key. + * Maybe empty, but not null. + * @param key The attribute defining which constraints shall be stored in a shared list, + * e.g. length of the constraints. + * @return The list of constraints where all constraints having the same key. + */ + public List getList(Key key) { + List constraints = map.get(key); + if (null == constraints) { + constraints = new ArrayList(); + map.put(key, constraints); + } + + return constraints; + } + + /** + * Returns a {@link Collection} of all {@link de.uni_hildesheim.sse.model.varModel.Constraint} lists. + * @return {@link Collection} of all {@link de.uni_hildesheim.sse.model.varModel.Constraint} lists. + */ + public Collection> allLists() { + return map.values(); + } + +} Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/LiteralFinder.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/LiteralFinder.java (revision 118) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/LiteralFinder.java (revision 118) @@ -0,0 +1,137 @@ +package de.uni_hildesheim.sse.trans.convert; + +import java.util.HashSet; +import java.util.Set; + +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.DslFragment; +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; + +/** + * Will find positive and negative declarations in a disjunction term. + * If a operation is not supported, this visitor will throw a {@link RuntimeException}. + * @author El-Sharkawy + * + */ +class LiteralFinder implements IConstraintTreeVisitor { + + private static final String NEGATIVE_PREFIX = "not("; + private static final String NEGATIVE_SUFFIX = ")"; + private boolean isPositive; + private Set declarations; + + /** + * Sole constructor for this class, starts the search. + * @param cst The {@link ConstraintSyntaxTree} where declarations shall be found. + */ + public LiteralFinder(ConstraintSyntaxTree cst) { + isPositive = true; + declarations = new HashSet(); + cst.accept(this); + } + + /** + * Returns all found declarations inside of the given constraint. + * @return All declarations, negated declarations will be returned as negated declarations. + */ + public Set getDeclarations() { + return declarations; + } + + @Override + public void visitConstantValue(ConstantValue value) { + throw new RuntimeException("Not Supported Operation"); + } + + @Override + public void visitVariable(Variable variable) { + if (isPositive) { + declarations.add(variable.getVariable().getName()); + } else { + declarations.add(NEGATIVE_PREFIX + variable.getVariable().getName() + NEGATIVE_SUFFIX); + } + } + + @Override + public void visitParenthesis(Parenthesis parenthesis) { + throw new RuntimeException("Not Supported Operation"); + } + + @Override + public void visitComment(Comment comment) { + throw new RuntimeException("Not Supported Operation"); + } + + @Override + public void visitOclFeatureCall(OCLFeatureCall call) { + if (OclKeyWords.OR.equals(call.getOperation())) { + call.getOperand().accept(this); + for (int i = 0, n = call.getParameterCount(); i < n; i++) { + call.getParameter(i).accept(this); + } + } else if (OclKeyWords.NOT.equals(call.getOperation())) { + isPositive = !isPositive; + call.getOperand().accept(this); + for (int i = 0, n = call.getParameterCount(); i < n; i++) { + call.getParameter(i).accept(this); + } + isPositive = !isPositive; + } else { + throw new RuntimeException("Not Supported Operation"); + } + } + + @Override + public void visitLet(Let let) { + throw new RuntimeException("Not Supported Operation"); + } + + @Override + public void visitIfThen(IfThen ifThen) { + throw new RuntimeException("Not Supported Operation"); + } + + @Override + public void visitContainerOperationCall(ContainerOperationCall call) { + throw new RuntimeException("Not Supported Operation"); + } + + @Override + public void visitCompoundAccess(CompoundAccess access) { + throw new RuntimeException("Not Supported Operation"); + } + + @Override + public void visitDslFragment(DslFragment fragment) { + throw new RuntimeException("Not Supported Operation"); + } + + @Override + public void visitUnresolvedExpression(UnresolvedExpression expression) { + throw new RuntimeException("Not Supported Operation"); + } + + @Override + public void visitCompoundInitializer(CompoundInitializer initializer) { + throw new RuntimeException("Not Supported Operation"); + } + + @Override + public void visitContainerInitializer(ContainerInitializer initializer) { + throw new RuntimeException("Not Supported Operation"); + } + +} Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ModelOptimizer.java =================================================================== --- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ModelOptimizer.java (revision 117) +++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/ModelOptimizer.java (revision 118) @@ -1,5 +1,5 @@ package de.uni_hildesheim.sse.trans.convert; -import java.util.ArrayList; +import java.util.Collection; import java.util.HashSet; import java.util.List; @@ -148,34 +148,37 @@ */ public int removeDuplicatedConstraints() { - List[] equivalenceClasses = createEquivalenceClasses(); + // Takes ~10 seconds + Collection> equivalenceClasses = createEquivalenceClasses(); int removed = 0; - - for (int h = 0; h < equivalenceClasses.length; h++) { - for (int i = 0, n = equivalenceClasses[h].size(); i < n; i++) { - Constraint constraint = equivalenceClasses[h].get(i); - if (constraint == null) { + int step = 1; + for (List constraintList : equivalenceClasses) { + LOGGER.info("Step " + step++ + " of " + equivalenceClasses.size()); + for (int i = 0, n = constraintList.size(); i < n - 1; i++) { + ConstraintContainer firstContainer = constraintList.get(i); + if (firstContainer == null) { continue; } - ConstraintSyntaxTree tree = constraint.getConsSyntax(); - DeclrationInConstraintFinder finder = new DeclrationInConstraintFinder(tree); - Set declarations = finder.getDeclarations(); + ConstraintSyntaxTree tree = firstContainer.getConstraint().getConsSyntax(); + Set firstLiterals = firstContainer.getLiterals(); + DeclrationInConstraintFinder declFinder = + new DeclrationInConstraintFinder(firstContainer.getConstraint().getConsSyntax()); + Set declarations = declFinder.getDeclarations(); + AbstractVariable[] declarationArray = declarations.toArray(new AbstractVariable[] {}); for (int j = i + 1; j < n; j++) { - Constraint otherConstraint = equivalenceClasses[h].get(j); - if (otherConstraint == null) { + ConstraintContainer otherContainer = constraintList.get(j); + if (otherContainer == null) { continue; } - ConstraintSyntaxTree otherTree = otherConstraint.getConsSyntax(); - DeclrationInConstraintFinder otherFinder = new DeclrationInConstraintFinder(otherTree); - Set otherDeclarations = otherFinder.getDeclarations(); + ConstraintSyntaxTree otherTree = otherContainer.getConstraint().getConsSyntax(); + Set secondLiterals = otherContainer.getLiterals(); - if (otherDeclarations.containsAll(declarations)) { + // Could be removed theoretically (double checking) + if (secondLiterals.containsAll(firstLiterals)) { boolean equal = true; - AbstractVariable[] declarationArray = declarations.toArray(new AbstractVariable[] {}); - for (int k = 0; k < declarationArray.length; k++) { if (isVariableNegated(tree, declarationArray[k]) @@ -187,6 +190,6 @@ if (equal) { - model.removeElement(otherConstraint); - equivalenceClasses[h].set(j, null); + model.removeElement(otherContainer.getConstraint()); + constraintList.set(j, null); removed++; } @@ -198,5 +201,5 @@ * set(index, null) avoids Array.copy */ - equivalenceClasses[h].set(i, null); + constraintList.set(i, null); } } @@ -233,23 +236,19 @@ /** * Split all constraints of the project into equivalence classes according to their length. - * @return An array of lists with constraint that all have the same length. - */ - private List[] createEquivalenceClasses() { + * @return An {@link Collection} of lists with constraint that all have the same length. + */ + private Collection> createEquivalenceClasses() { ConstraintFinder cFinder = new ConstraintFinder(model); List constraints = cFinder.getConstraints(); - List[] equivalenceClasses = new List[10]; // TODO 10? - for (int i = 0; i < equivalenceClasses.length; i++) { - equivalenceClasses[i] = new ArrayList(); - } + ConstraintMap map = new ConstraintMap(); for (int i = 0, n = constraints.size(); i < n; i++) { Constraint constraint = constraints.get(i); ConstraintSyntaxTree tree = constraint.getConsSyntax(); - DeclrationInConstraintFinder finder = new DeclrationInConstraintFinder(tree); - Set declarations = finder.getDeclarations(); - - int length = Math.min(declarations.size(), equivalenceClasses.length); - equivalenceClasses[length - 1].add(constraint); + LiteralFinder finder = new LiteralFinder(tree); + Set declarations = finder.getDeclarations(); + + map.getList(declarations.size()).add(new ConstraintContainer(constraint, declarations)); /* @@ -259,5 +258,5 @@ constraints.set(i, null); } - return equivalenceClasses; + return map.allLists(); }