Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/Main.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/Main.java (revision 94)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/Main.java (revision 95)
@@ -9,4 +9,5 @@
import de.uni_hildesheim.sse.utils.logger.AdvancedJavaLogger;
import de.uni_hildesheim.sse.utils.logger.EASyLoggerFactory;
+import de.uni_hildesheim.sse.utils.logger.LoggingLevel;
/**
@@ -19,4 +20,5 @@
static {
EASyLoggerFactory.INSTANCE.setLogger(new AdvancedJavaLogger());
+ EASyLoggerFactory.INSTANCE.setLoggingLevel(LoggingLevel.INFO);
}
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/cli/ArgumentsParser.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/cli/ArgumentsParser.java (revision 94)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/cli/ArgumentsParser.java (revision 95)
@@ -42,7 +42,4 @@
OPTIONS.addOption(CMD_HELP, "help", false, "Prints this help instead of perfoming the model translation");
OPTIONS.addOption(CMD_VERSION, "version", true, "Optional: The version of the source model (in IVML syntax)");
-
- EASyLoggerFactory.INSTANCE.setLogger(new AdvancedJavaLogger());
- EASyLoggerFactory.INSTANCE.setLoggingLevel(LoggingLevel.INFO);
}
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2.java (revision 94)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2.java (revision 95)
@@ -1,3 +1,6 @@
package de.uni_hildesheim.sse.trans.convert;
+
+import java.math.BigInteger;
+import java.text.NumberFormat;
import de.uni_hildesheim.sse.model.confModel.AssignmentState;
@@ -18,8 +21,17 @@
*
* @author Adam Krafczyk
+ * @author El-Sharkawy
*/
public class MaxTermConverter2 extends MaxTermConverter {
private static final EASyLogger LOGGER = EASyLoggerFactory.INSTANCE.getLogger(MaxTermConverter2.class, Bundle.ID);
-
+ private static final BigInteger TWO = BigInteger.valueOf(2);
+ private static final NumberFormat PERCENT_FORMAT = NumberFormat.getPercentInstance();
+ static {
+ PERCENT_FORMAT.setMaximumFractionDigits(3);
+ }
+
+ private long lastTime;
+ private BigInteger totalSteps;
+ private BigInteger elapsedSteps;
@Override
@@ -27,4 +39,7 @@
Configuration config) {
+ lastTime = System.currentTimeMillis();
+ totalSteps = TWO.pow(declarationArray.length);
+ elapsedSteps = BigInteger.ZERO;
handleConstraint(originalConstraint, declarationArray, config, 0);
}
@@ -34,4 +49,7 @@
Configuration config) {
+ lastTime = System.currentTimeMillis();
+ totalSteps = TWO.pow(declarationArray.length);
+ elapsedSteps = BigInteger.ZERO;
handleConstraint(originalConstraint, declarationArray, config, 0);
}
@@ -46,6 +64,12 @@
* @param var the variable to change
*/
- protected void handleConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray,
- Configuration config, int var) {
+ private void handleConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray,
+ Configuration config, int var) {
+
+ if (System.currentTimeMillis() - lastTime > 10000) {
+ lastTime = System.currentTimeMillis();
+ LOGGER.info("Progress: (" + declarationArray.length + " vars) "
+ + PERCENT_FORMAT.format(elapsedSteps.doubleValue() / totalSteps.doubleValue()));
+ }
if (var >= declarationArray.length) {
@@ -57,18 +81,19 @@
decisionVar.setValue(BooleanValue.TRUE, AssignmentState.ASSIGNED);
- int result = checkConstraint(originalConstraint, config);
- if (result == 0) {
- addExpression(declarationArray, var, config);
- } else if (result == -1) {
- handleConstraint(originalConstraint, declarationArray, config, var + 1);
- }
+ checkConstraint(originalConstraint, declarationArray, config, var);
+// if (result == 0) {
+// addExpression(declarationArray, var, config);
+// } else if (result == -1) {
+// handleConstraint(originalConstraint, declarationArray, config, var + 1);
+// }
decisionVar.setValue(BooleanValue.FALSE, AssignmentState.ASSIGNED);
- result = checkConstraint(originalConstraint, config);
- if (result == 0) {
- addExpression(declarationArray, var, config);
- } else if (result == -1) {
- handleConstraint(originalConstraint, declarationArray, config, var + 1);
- }
+// result = checkConstraint(originalConstraint, config);
+ checkConstraint(originalConstraint, declarationArray, config, var);
+// if (result == 0) {
+// addExpression(declarationArray, var, config);
+// } else if (result == -1) {
+// handleConstraint(originalConstraint, declarationArray, config, var + 1);
+// }
decisionVar.setValue(null, AssignmentState.UNDEFINED);
@@ -76,4 +101,38 @@
} catch (ConfigurationException e) {
LOGGER.exception(e);
+ }
+ }
+
+ /**
+ * Part of the {@link #handleConstraint(ConstraintSyntaxTree, AbstractVariable[], Configuration, int)} method.
+ * Calls {@link #checkConstraint(ConstraintSyntaxTree, Configuration)} and starts a recusive call of the
+ * {@link #handleConstraint(ConstraintSyntaxTree, AbstractVariable[], Configuration, int)} method if needed.
+ * @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 var the variable to change
+ */
+ private void checkConstraint(ConstraintSyntaxTree originalConstraint, AbstractVariable[] declarationArray,
+ Configuration config, int var) {
+
+ int result = checkConstraint(originalConstraint, config);
+ switch (result) {
+ case 0:
+ BigInteger skipped = TWO.pow(declarationArray.length - (var + 1));
+ elapsedSteps = elapsedSteps.add(skipped);
+ addExpression(declarationArray, var, config);
+ break;
+ case -1:
+ handleConstraint(originalConstraint, declarationArray, config, var + 1);
+ break;
+ case 1:
+ skipped = TWO.pow(declarationArray.length - (var + 1));
+ elapsedSteps = elapsedSteps.add(skipped);
+ break;
+ default:
+ LOGGER.error("Unexpected while creating max terms.");
+ break;
}
}
Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2Test.java
===================================================================
--- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2Test.java (revision 94)
+++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverter2Test.java (revision 95)
@@ -4,4 +4,7 @@
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.ConstraintSyntaxTree;
@@ -9,4 +12,5 @@
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;
@@ -15,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;
/**
@@ -72,4 +77,59 @@
/**
+ * Tests whether the {@link EvaluationVisitor}, which is used inside of {@link MaxTermConverter2}, is sufficient
+ * for {@link MaxTermConverter}.
+ */
+ @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
+ */
+ // Tests whether b = true and c = false are sufficient to evaluate the constraint to false.
+ 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);
+
+ Assert.assertTrue(evaluator.constraintFailed());
+ }
+
+ /**
* Tests whether a constraint only contains OR's and NOT's.
* @param tree The constraint to be tested.
Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java
===================================================================
--- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java (revision 94)
+++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/convert/MaxTermConverterTest.java (revision 95)
@@ -4,7 +4,4 @@
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.ConstraintSyntaxTree;
@@ -12,5 +9,4 @@
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;
@@ -19,5 +15,4 @@
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;
/**
@@ -124,59 +119,3 @@
}
}
-
- /**
- * Tests whether the {@link EvaluationVisitor}, which is used inside of {@link MaxTermConverter}, is sufficient
- * for {@link MaxTermConverter}.
- */
- @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
- */
- // Tests whether b = true and c = false are sufficient to evaluate the constraint to false.
- 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);
-
- Assert.assertTrue(evaluator.constraintFailed());
- }
-
}