Index: /Code/ModelTranslator/resources/ToDo.txt
===================================================================
--- /Code/ModelTranslator/resources/ToDo.txt	(revision 379)
+++ /Code/ModelTranslator/resources/ToDo.txt	(revision 380)
@@ -5,5 +5,5 @@
   
 * Choices behandeln (fuer Beispiel siehe CHOICE_7 und GENERIC_CPU)
- - in DIMACS: Umwandeln in XOR Constraints (oder entsprechende CNF-Constraints)
+ - (done) in DIMACS: Umwandeln in XOR Constraints (oder entsprechende CNF-Constraints)
  - in IVML: Umwandeln in Enumerationen
  
Index: /Code/ModelTranslator/resources/testdata/input/testModel_Choices.rsf
===================================================================
--- /Code/ModelTranslator/resources/testdata/input/testModel_Choices.rsf	(revision 380)
+++ /Code/ModelTranslator/resources/testdata/input/testModel_Choices.rsf	(revision 380)
@@ -0,0 +1,19 @@
+#startchoice
+Choice	CHOICE_12	required	boolean
+#choice value
+ChoiceItem	HZ_100	CHOICE_12
+Item	HZ_100	boolean
+Depends	HZ_100	"CHOICE_12"
+#choice value
+ChoiceItem	HZ_250	CHOICE_12
+Item	HZ_250	boolean
+Depends	HZ_250	"CHOICE_12"
+#choice value
+ChoiceItem	HZ_300	CHOICE_12
+Item	HZ_300	boolean
+Depends	HZ_300	"CHOICE_12"
+#choice value
+ChoiceItem	HZ_1000	CHOICE_12
+Item	HZ_1000	boolean
+Depends	HZ_1000	"CHOICE_12"
+#endchoice
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/in/rsf/RSFChoice.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/in/rsf/RSFChoice.java	(revision 379)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/in/rsf/RSFChoice.java	(revision 380)
@@ -47,24 +47,21 @@
     ConstraintSyntaxTree[] getBooleanConstraintSyntaxTree(AbstractReader reader) {
         // Create choiceItems.size() Constraints with all choiceItems OR'd together and 1 negated each.
+        // Also contains NOT choiceName since the choice only applies if choiceName is true
+        
         ConstraintSyntaxTree[] trees = new ConstraintSyntaxTree[choiceItems.size()];
+        Variable choiceVar = varPool.obtainVariable(reader.getVariable(choiceName));
         
         for (int i = 0; i < trees.length; i++) {
             
+            trees[i] = new OCLFeatureCall(choiceVar, OclKeyWords.NOT);
+            
             for (int j = 0; j < choiceItems.size(); j++) {
-                Variable var = varPool.obtainVariable(reader.getVariable(choiceItems.get(i)));
+                Variable var = varPool.obtainVariable(reader.getVariable(choiceItems.get(j)));
                 // variable #i should be negated
                 if (j == i) {
-                    if (trees[i] == null) {
-                        trees[i] = new OCLFeatureCall(var, OclKeyWords.NOT);
-                    } else {
-                        trees[i] = new OCLFeatureCall(trees[i], OclKeyWords.OR,
-                                new OCLFeatureCall(var, OclKeyWords.NOT));
-                    }
+                    trees[i] = new OCLFeatureCall(trees[i], OclKeyWords.OR,
+                            new OCLFeatureCall(var, OclKeyWords.NOT));
                 } else {
-                    if (trees[i] == null) {
-                        trees[i] = var;
-                    } else {
-                        trees[i] = new OCLFeatureCall(trees[i], OclKeyWords.OR, var);
-                    }
+                    trees[i] = new OCLFeatureCall(trees[i], OclKeyWords.OR, var);
                 }
             }
@@ -72,6 +69,4 @@
         }
         
-        // TODO only if choice is true
-        
         return trees;
     }
Index: /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/in/rsf/RSFReader.java
===================================================================
--- /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/in/rsf/RSFReader.java	(revision 379)
+++ /Code/ModelTranslator/src/de/uni_hildesheim/sse/trans/in/rsf/RSFReader.java	(revision 380)
@@ -202,5 +202,5 @@
         }
         
-        // Add conditions
+        // 3. Add conditions
         for (RSFCondition condition : conditions) {
             try {
@@ -215,4 +215,6 @@
             }
         }
+        
+        // 4. TODO: Add choice conditions
     }
 
Index: /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/scenario/RsfToDimacsTranslationTest.java
===================================================================
--- /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/scenario/RsfToDimacsTranslationTest.java	(revision 379)
+++ /Code/ModelTranslator/test/de/uni_hildesheim/sse/trans/scenario/RsfToDimacsTranslationTest.java	(revision 380)
@@ -106,4 +106,40 @@
             DimacsTestUtils.containsConstraint(result, arch32, arch64, -1 * bit));
     }
+    
+    /**
+     * Tests whether choices are translated correctly into CNF constraints.
+     */
+    @Test
+    public void testChoices() {
+        File input = new File(AllTests.INPUT_FOLDER, "testModel_Choices.rsf");
+        OptimizationParameter noOptimization = new OptimizationParameter();
+        
+        // Test precondition
+        Assert.assertFalse(noOptimization.hasAtLeastOneOption());
+        
+        // Translation
+        String result = DimacsTestUtils.loadModel(input, noOptimization, true);
+        int choice12 = DimacsTestUtils.getNumberOfVariable(result, "CHOICE_12");
+        int hz100 = DimacsTestUtils.getNumberOfVariable(result, "HZ_100");
+        int hz250 = DimacsTestUtils.getNumberOfVariable(result, "HZ_250");
+        int hz300 = DimacsTestUtils.getNumberOfVariable(result, "HZ_300");
+        int hz1000 = DimacsTestUtils.getNumberOfVariable(result, "HZ_1000");
+        
+        /*
+         * Test whether the following constraints are included:
+         * NOT(CHOICE_12) OR NOT(HZ_100) OR HZ_250 OR HZ_300 OR HZ_1000
+         * NOT(CHOICE_12) OR HZ_100 OR NOT(HZ_250) OR HZ_300 OR HZ_1000
+         * NOT(CHOICE_12) OR HZ_100 OR HZ_250 OR NOT(HZ_300) OR HZ_1000
+         * NOT(CHOICE_12) OR HZ_100 OR HZ_250 OR HZ_300 OR NOT(HZ_1000)
+         */
+        Assert.assertTrue("Error: Missing choice constraint",
+                DimacsTestUtils.containsConstraint(result, -1 * choice12, -1 * hz100, hz250, hz300, hz1000));
+        Assert.assertTrue("Error: Missing choice constraint",
+                DimacsTestUtils.containsConstraint(result, -1 * choice12, hz100, -1 * hz250, hz300, hz1000));
+        Assert.assertTrue("Error: Missing choice constraint",
+                DimacsTestUtils.containsConstraint(result, -1 * choice12, hz100, hz250, -1 * hz300, hz1000));
+        Assert.assertTrue("Error: Missing choice constraint",
+                DimacsTestUtils.containsConstraint(result, -1 * choice12, hz100, hz250, hz300, -1 * hz1000));
+    }
 
 }