Index: /Code/ModelTranslator/resources/testdata/input/testModel_DefaultAndPrompts.rsf =================================================================== --- /Code/ModelTranslator/resources/testdata/input/testModel_DefaultAndPrompts.rsf (revision 378) +++ /Code/ModelTranslator/resources/testdata/input/testModel_DefaultAndPrompts.rsf (revision 378) @@ -0,0 +1,10 @@ +#Testing defaults in combination with prompts: +# -> ARCH has default and no prompt -> ARCH='x86_64' must be constant +# -> 64BIT only a prompt if ARCH='x86' -> 64BIT=true must be constant +Item ARCH string +HasPrompts ARCH 0 +Default ARCH 'x86_64' y +Item 64BIT boolean +Prompt 64BIT ARCH='x86' +HasPrompts 64BIT 1 +Default 64BIT ARCH='x86_64' y Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/DimacsTestUtils.java =================================================================== --- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/DimacsTestUtils.java (revision 378) +++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/DimacsTestUtils.java (revision 378) @@ -0,0 +1,119 @@ +package de.uni_hildesheim.sse.trans; + +import java.io.File; +import java.io.StringWriter; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import org.junit.Assert; + +import de.uni_hildesheim.sse.model.varModel.IvmlKeyWords; +import de.uni_hildesheim.sse.trans.convert.OptimizationParameter; +import de.uni_hildesheim.sse.trans.in.InputType; +import de.uni_hildesheim.sse.trans.out.DimacsWriter; +import de.uni_hildesheim.sse.trans.out.OutputType; + +/** + * Helping methods for testing translation into dimacs. + * @author El-Sharkawy + * + */ +public class DimacsTestUtils { + + /** + * Unused constructor. + */ + private DimacsTestUtils() { + // Not needed as this is only a utility class with static methods. + } + + /** + * Loads the given input file and transforms it into a DIMACS model using the given optimizations. + * @param input The input file to load (must exist). + * @param optimizations Specification which optimizations shall be applied to the transformed model. Will only be + * applied to transformations into CNF. + * @param removePreamble true the preamble (comment, version, and a help information) will be removed + * from the beginning of this string). + * @return The translated DIMACS model. + */ + public static String loadModel(File input, OptimizationParameter optimizations, boolean removePreamble) { + String comment = "A comment"; + String version = "0.1"; + StringWriter sWriter = new StringWriter(); + + // Test precondition + Assert.assertTrue(input.exists()); + + // Translation + ModelTranslator.translate(input, sWriter, InputType.RSF, OutputType.DIMCAS, comment, version, optimizations); + String result = sWriter.toString(); + + // Test correct translation of comment, version, and help + Assert.assertNotNull(result); + Assert.assertTrue("Error in preamble.", + result.startsWith( + "c " + comment + IvmlKeyWords.LINEFEED + + "c Version " + version + IvmlKeyWords.LINEFEED + + DimacsWriter.HELP)); + + if (removePreamble) { + result = removePreamble(result); + } + + return result; + } + + /** + * Removes the preamble of a already translated dimacs model. + * @param dimacsModel The model where the preamble shall be deleted + * @return Only the relevant information of the translated dimacs model. + */ + private static String removePreamble(String dimacsModel) { + int beginning = dimacsModel.indexOf(DimacsWriter.HELP); + return dimacsModel.substring(beginning + DimacsWriter.HELP.length()); + } + + /** + * Returns the DIMACs number of the given variable which is used inside the constraints. + * @param dimacsModel The complete dimacs model + * @param variable The variable for which the number shall be retrieved. + * @return The number of the variable used inside the constraints. + */ + public static int getNumberOfVariable(String dimacsModel, String variable) { + Pattern dimacsVarDefintion = Pattern.compile("(?m)^c (\\d+) " + variable + "$"); + Matcher m = dimacsVarDefintion.matcher(dimacsModel); + String result = null; + if (m.find()) { + result = m.group(1); + } + + Assert.assertNotNull("Error: Variable not found.", result); + + + return Integer.valueOf(result); + } + + /** + * Checks whether a given constraint is included in dimacsModel. + * @param dimacsModel The complete dimacs model + * @param literals positive and negative variable numbers (must not be 0). + * @return true if the constraint is included in dimacsModel. + */ + public static boolean containsConstraint(String dimacsModel, int... literals) { + StringBuffer constraintDef = new StringBuffer("(?m)^("); + constraintDef.append(literals[0]); + constraintDef.append(" "); + for (int i = 1; i < literals.length; i++) { + constraintDef.append("|"); + constraintDef.append(literals[i]); + constraintDef.append(" "); + } + constraintDef.append("){"); + constraintDef.append(literals.length); + constraintDef.append("}0$"); + + Pattern constraintDefinition = Pattern.compile(constraintDef.toString()); + Matcher m = constraintDefinition.matcher(dimacsModel); + return m.find(); + } +} Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/scenario/RsfToDimacsTranslationTest.java =================================================================== --- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/scenario/RsfToDimacsTranslationTest.java (revision 377) +++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/scenario/RsfToDimacsTranslationTest.java (revision 378) @@ -2,18 +2,12 @@ import java.io.File; -import java.io.StringWriter; -import java.util.regex.Matcher; -import java.util.regex.Pattern; import org.junit.Assert; +import org.junit.Ignore; import org.junit.Test; -import de.uni_hildesheim.sse.model.varModel.IvmlKeyWords; import de.uni_hildesheim.sse.trans.AllTests; -import de.uni_hildesheim.sse.trans.ModelTranslator; +import de.uni_hildesheim.sse.trans.DimacsTestUtils; import de.uni_hildesheim.sse.trans.convert.OptimizationParameter; -import de.uni_hildesheim.sse.trans.in.InputType; -import de.uni_hildesheim.sse.trans.out.DimacsWriter; -import de.uni_hildesheim.sse.trans.out.OutputType; /** @@ -23,94 +17,4 @@ */ public class RsfToDimacsTranslationTest { - - /** - * Loads the given input file and transforms it into a DIMACS model using the given optimizations. - * @param input The input file to load (must exist). - * @param optimizations Specification which optimizations shall be applied to the transformed model. Will only be - * applied to transformations into CNF. - * @param removePreamble true the preamble (comment, version, and a help information) will be removed - * from the beginning of this string). - * @return The translated DIMACS model. - */ - private static String loadModel(File input, OptimizationParameter optimizations, boolean removePreamble) { - String comment = "A comment"; - String version = "0.1"; - StringWriter sWriter = new StringWriter(); - - // Test precondition - Assert.assertTrue(input.exists()); - - // Translation - ModelTranslator.translate(input, sWriter, InputType.RSF, OutputType.DIMCAS, comment, version, optimizations); - String result = sWriter.toString(); - - // Test correct translation of comment, version, and help - Assert.assertNotNull(result); - Assert.assertTrue("Error in preamble.", - result.startsWith( - "c " + comment + IvmlKeyWords.LINEFEED - + "c Version " + version + IvmlKeyWords.LINEFEED - + DimacsWriter.HELP)); - - if (removePreamble) { - result = removePreamble(result); - } - - return result; - } - - /** - * Removes the preamble of a already translated dimacs model. - * @param dimacsModel The model where the preamble shall be deleted - * @return Only the relevant information of the translated dimacs model. - */ - private static String removePreamble(String dimacsModel) { - int beginning = dimacsModel.indexOf(DimacsWriter.HELP); - return dimacsModel.substring(beginning + DimacsWriter.HELP.length()); - } - - /** - * Returns the DIMACs number of the given variable which is used inside the constraints. - * @param dimacsModel The complete dimacs model - * @param variable The variable for which the number shall be retrieved. - * @return The number of the variable used inside the constraints. - */ - private static int getNumberOfVariable(String dimacsModel, String variable) { - Pattern dimacsVarDefintion = Pattern.compile("(?m)^c (\\d+) " + variable + "$"); - Matcher m = dimacsVarDefintion.matcher(dimacsModel); - String result = null; - if (m.find()) { - result = m.group(1); - } - - Assert.assertNotNull("Error: Variable not found.", result); - - - return Integer.valueOf(result); - } - - /** - * Checks whether a given constraint is included in dimacsModel. - * @param dimacsModel The complete dimacs model - * @param literals positive and negative variable numbers (must not be 0). - * @return true if the constraint is included in dimacsModel. - */ - private static boolean containsConstraint(String dimacsModel, int... literals) { - StringBuffer constraintDef = new StringBuffer("(?m)^("); - constraintDef.append(literals[0]); - constraintDef.append(" "); - for (int i = 1; i < literals.length; i++) { - constraintDef.append("|"); - constraintDef.append(literals[i]); - constraintDef.append(" "); - } - constraintDef.append("){"); - constraintDef.append(literals.length); - constraintDef.append("}0$"); - - Pattern constraintDefinition = Pattern.compile(constraintDef.toString()); - Matcher m = constraintDefinition.matcher(dimacsModel); - return m.find(); - } /** @@ -126,5 +30,5 @@ // Translation - String result = loadModel(input, noOptimization, true); + String result = DimacsTestUtils.loadModel(input, noOptimization, true); System.out.println(result); @@ -145,10 +49,11 @@ // Translation - String result = loadModel(input, noOptimization, true); - int iwc3200top = getNumberOfVariable(result, "IWMC3200TOP") * -1; - int fwLoader = getNumberOfVariable(result, "FW_LOADER"); - int blubb = getNumberOfVariable(result, "BLUBB") * -1; + String result = DimacsTestUtils.loadModel(input, noOptimization, true); + int iwc3200top = DimacsTestUtils.getNumberOfVariable(result, "IWMC3200TOP") * -1; + int fwLoader = DimacsTestUtils.getNumberOfVariable(result, "FW_LOADER"); + int blubb = DimacsTestUtils.getNumberOfVariable(result, "BLUBB") * -1; - /* Test whether following constraint is included: + /* + * Test whether following constraint is included: * Not(IWMC3200TOP AND BLUBB) or FW_LOADER * --> @@ -156,5 +61,48 @@ */ Assert.assertTrue("Error: Expected Constraint not included.", - containsConstraint(result, iwc3200top, blubb, fwLoader)); + DimacsTestUtils.containsConstraint(result, iwc3200top, blubb, fwLoader)); + } + + /** + * Tests whether the combination of prompts and default values are considered. Tests: + * + */ + @Ignore("Currently, not supported") + @Test + public void testDefaultsAndPrompts() { + File input = new File(AllTests.INPUT_FOLDER, "testModel_DefaultAndPrompts.rsf"); + OptimizationParameter noOptimization = new OptimizationParameter(); + + // Test precondition + Assert.assertFalse(noOptimization.hasAtLeastOneOption()); + + // Translation + String result = DimacsTestUtils.loadModel(input, noOptimization, true); + System.out.println(result); + int arch32 = DimacsTestUtils.getNumberOfVariable(result, "ARCH='x86'"); + int arch64 = DimacsTestUtils.getNumberOfVariable(result, "ARCH='x86_64'"); + int bit = DimacsTestUtils.getNumberOfVariable(result, "64BIT"); + + /* + * Test whether following 3 constraints are included: + * - ARCH='x86_64' + * - ARCH='x86_64' implies 64BIT + * -> Not(ARCH='x86_64') or 64BIT + * - ARCH='x86' implies (64BIT or !64BIT) + * -> tautology -> skip this constraint + * - (!ARCH='x86_64' and !ARCH='x86') implies !64Bit (combination of prompt and default) + * -> ARCH='x86_64' or ARCH='x86' or !64BIT + */ + Assert.assertTrue("Error: ARCH='x86_64' constant not included", + DimacsTestUtils.containsConstraint(result, arch64)); + Assert.assertTrue("Error: 64Bit default not included", + DimacsTestUtils.containsConstraint(result, -1 * arch64, bit)); + Assert.assertTrue("Error: 64Bit default and prompt not included", + DimacsTestUtils.containsConstraint(result, arch32, arch64, -1 * bit)); }