diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 5ee14561fdf7963f94bb46f00b8fff6a733bfe81..911a8639c81c3b4da0d36868aec5fce449f0a275 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -153,7 +153,7 @@ public class Translator {
 		configString = printer.getConfigString().toString();
 
 		tlcOutputInfo = new TLCOutputInfo(machineContext, renamer,
-				typechecker, generator.getTlaModule());
+				typechecker, generator.getTlaModule(), generator.getConfigFile());
 	}
 
 	public String getMachineString() {
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index 69e237151d5b0f97dbc804bfebbdd432fcbaa03c..6be0cea9aba6182e073cfd20aab9e4aaf3011737 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -10,7 +10,10 @@ import de.tlc4b.analysis.MachineContext;
 import de.tlc4b.analysis.Renamer;
 import de.tlc4b.analysis.Typechecker;
 import de.tlc4b.btypes.BType;
+import de.tlc4b.tla.ConfigFile;
 import de.tlc4b.tla.TLAModule;
+import de.tlc4b.tla.config.ConfigFileAssignment;
+import de.tlc4b.tla.config.ModelValueAssignment;
 
 public class TLCOutputInfo {
 
@@ -45,7 +48,7 @@ public class TLCOutputInfo {
 	}
 
 	public TLCOutputInfo(MachineContext machineContext, Renamer renamer,
-			Typechecker typechecker, TLAModule tlaModule) {
+			Typechecker typechecker, TLAModule tlaModule, ConfigFile configFile) {
 
 		this.namesMapping = new Hashtable<String, String>();
 		this.typesTable = new Hashtable<String, BType>();
@@ -60,7 +63,8 @@ public class TLCOutputInfo {
 		identifiers.putAll(machineContext.getConstants());
 		identifiers.putAll(machineContext.getVariables());
 		identifiers.putAll(machineContext.getEnumValues());
-
+		//TODO add sets of modelvalues
+		
 		
 		for (Entry<String, Node> entry : identifiers.entrySet()) {
 			String name = entry.getKey();
diff --git a/src/main/java/de/tlc4b/tlc/TracePrinter.java b/src/main/java/de/tlc4b/tlc/TracePrinter.java
index 9260f4d21eef88a90bbebcb343e19b3cdfca6690..4bf91aa304b91032e0dea1b5804351c5b2d3067d 100644
--- a/src/main/java/de/tlc4b/tlc/TracePrinter.java
+++ b/src/main/java/de/tlc4b/tlc/TracePrinter.java
@@ -7,6 +7,7 @@ import de.tlc4b.btypes.FunctionType;
 import de.tlc4b.btypes.PairType;
 import de.tlc4b.btypes.SetType;
 import de.tlc4b.btypes.StructType;
+import de.tlc4b.exceptions.NotSupportedException;
 import tla2sany.semantic.OpDeclNode;
 import tlc2.tool.TLCState;
 import tlc2.tool.TLCStateInfo;
@@ -185,7 +186,7 @@ public class TracePrinter {
 				}
 
 			}
-			return null;
+			throw new NotSupportedException("Unkown type of tuple.");
 
 		case RECORDVALUE: {
 			RecordValue rec = (RecordValue) val;
@@ -223,8 +224,11 @@ public class TracePrinter {
 
 		case MODELVALUE:
 			ModelValue modelValue = (ModelValue) val;
-			String BName = tlcOutputInfo.getBName(modelValue.toString());
-			res.append(BName);
+			String bName = tlcOutputInfo.getBName(modelValue.toString());
+			if(bName == null){
+				bName = modelValue.toString();
+			}
+			res.append(bName);
 			return res;
 
 		case SETOFTUPLESVALUE: {
diff --git a/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java
index 180a91334c1d5d0a808b42bb8e10abe1316d2a14..a078bd7eff1b03b98da268967fc54aeda4b73399 100644
--- a/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java
@@ -33,7 +33,6 @@ public class SpecialTest {
 		assertEquals(NoError, test(a));
 	}
 	
-	
 	@Test
 	public void testConstantSetupFile2() throws Exception {
 		String[] a = new String[] {
@@ -49,7 +48,6 @@ public class SpecialTest {
 		assertEquals(Deadlock, test(a));
 	}
 	
-	
 	@Test
 	public void testDefinitionsLoad() throws Exception {
 		String[] a = new String[] {