fixed constants setup in trace file

build.gradle

@@ -37,7 +37,7 @@ dependencies {
 
 	testCompile (group: 'junit', name: 'junit', version: '4.7')
 	testCompile (group: 'de.prob', name: 'tla2b', version: '1.0.4-SNAPSHOT')
-    
+    testCompile (group: 'de.prob', name: 'tla2bAST', version: '1.0.0-SNAPSHOT')
 
 	releaseJars (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT')
 	releaseJars (group: 'de.prob', name: 'prologlib', version: parser_version)

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 tla2sany.semantic.OpDeclNode;
 import tlc2.tool.TLCState;
 import tlc2.tool.TLCStateInfo;
 import tlc2.value.FcnLambdaValue;
@@ -38,6 +39,9 @@ public class TracePrinter {
 	TLCState initialState;
 	TLCOutputInfo tlcOutputInfo;
 
+	ArrayList<OpDeclNode> constants;
+	ArrayList<OpDeclNode> variables;
+
 	StringBuilder traceBuilder;
 
 	public TracePrinter(ArrayList<TLCStateInfo> trace,
@@ -45,9 +49,19 @@ public class TracePrinter {
 		this.trace = trace;
 		this.tlcOutputInfo = tlcOutputInfo;
 
-		evalTrace();
+		constants = new ArrayList<OpDeclNode>();
+		variables = new ArrayList<OpDeclNode>();
+		for (int i = 0; i < TLCState.vars.length; i++) {
+			String id = TLCState.vars[i].getName().toString();
+			if (tlcOutputInfo.constants.contains(id)) {
+				constants.add(TLCState.vars[i]);
+			} else {
+				variables.add(TLCState.vars[i]);
+			}
 		}
 
+		evalTrace();
+	}
 
 	public TracePrinter(TLCState initialState, TLCOutputInfo tlcOutputInfo) {
 		this.initialState = initialState;
@@ -59,11 +73,11 @@ public class TracePrinter {
 		return traceBuilder;
 	}
 
-
 	private void evalTrace() {
 		traceBuilder = new StringBuilder();
 		
 		if (trace != null) {
+			traceBuilder.append(setupConstants(trace.get(0).state));
 			for (int i = 0; i < trace.size(); i++) {
 				if (i > 0) {
 					traceBuilder.append("\n");
@@ -71,20 +85,43 @@ public class TracePrinter {
 				traceBuilder.append(evalExpression(trace.get(i).state));
 			}
 		} else {
+			traceBuilder.append(setupConstants(initialState));
 			traceBuilder.append(evalExpression(initialState));
 		}
 
 		// System.out.println(traceBuilder);
 	}
 
+	private StringBuilder setupConstants(TLCState state) {
+		StringBuilder expression = new StringBuilder();
+		if (tlcOutputInfo.constantSetup) {
+			if(constants.size() == 0){
+				expression.append("1 = 1");
+			}else{
+				for (int i = 0; i < constants.size(); i++) {
+					if (i > 0) {
+						expression.append(" & ");
+					}
+					UniqueString var = constants.get(i).getName();
+					BType type = tlcOutputInfo.getBType(var.toString());
+					String value = parseValue(state.lookup(var), type)
+							.toString();
+					expression.append(var).append(" = ").append(value);
+				}
+			}
+			expression.append("\n");
+		}
+		return expression;
+	}
+
 	private StringBuilder evalExpression(TLCState state) {
 		StringBuilder expression = new StringBuilder();
 
-		for (int i = 0; i < TLCState.vars.length; i++) {
+		for (int i = 0; i < variables.size(); i++) {
 			if (i > 0) {
 				expression.append(" & ");
 			}
-			UniqueString var = TLCState.vars[i].getName();
+			UniqueString var = variables.get(i).getName();
 			BType type = tlcOutputInfo.getBType(var.toString());
 			String value = parseValue(state.lookup(var), type).toString();
 			expression.append(var).append(" = ").append(value);
@@ -154,7 +191,6 @@ public class TracePrinter {
 			return res;
 		}
 
-
 		case FCNRCDVALUE:
 			FcnRcdValue function = (FcnRcdValue) val;
 			FunctionType funcType = (FunctionType) type;
@@ -214,7 +250,8 @@ public class TracePrinter {
 		case SUBSETVALUE: {
 			SubsetValue s = (SubsetValue) val;
 			SetType t = (SetType) type;
-			res.append("POW(").append(parseValue(s.set, t.getSubtype())).append(")");
+			res.append("POW(").append(parseValue(s.set, t.getSubtype()))
+					.append(")");
 			return res;
 		}
 		case UNIONVALUE: {
@@ -279,7 +316,6 @@ public class TracePrinter {
 			return res;
 		}
 
-
 		}
 		System.err.println("Type: " + val.getKind());
 		throw new RuntimeException("not supported construct: " + val);

src/test/java/testing/Testing2.java

@@ -29,8 +29,8 @@ public class Testing2 extends AbstractParseMachineTest{
 	@Test
 	public void testRunTLC() throws Exception {
 		String[] a = new String[] {machine.getPath()};
-		//TLC4B.main(a);
-		TLC4B.test(a,false);
+		TLC4B.main(a);
+		//TLC4B.test(a,false);
 	}
 
 	@Config