Skip to content
Snippets Groups Projects
Commit 78ab86c8 authored by hansen's avatar hansen
Browse files

Fixed a bug in the TracePrinter

parent f907e152
Branches
Tags
No related merge requests found
...@@ -153,7 +153,7 @@ public class Translator { ...@@ -153,7 +153,7 @@ public class Translator {
configString = printer.getConfigString().toString(); configString = printer.getConfigString().toString();
tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, tlcOutputInfo = new TLCOutputInfo(machineContext, renamer,
typechecker, generator.getTlaModule()); typechecker, generator.getTlaModule(), generator.getConfigFile());
} }
public String getMachineString() { public String getMachineString() {
......
...@@ -10,7 +10,10 @@ import de.tlc4b.analysis.MachineContext; ...@@ -10,7 +10,10 @@ import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.Renamer; import de.tlc4b.analysis.Renamer;
import de.tlc4b.analysis.Typechecker; import de.tlc4b.analysis.Typechecker;
import de.tlc4b.btypes.BType; import de.tlc4b.btypes.BType;
import de.tlc4b.tla.ConfigFile;
import de.tlc4b.tla.TLAModule; import de.tlc4b.tla.TLAModule;
import de.tlc4b.tla.config.ConfigFileAssignment;
import de.tlc4b.tla.config.ModelValueAssignment;
public class TLCOutputInfo { public class TLCOutputInfo {
...@@ -45,7 +48,7 @@ public class TLCOutputInfo { ...@@ -45,7 +48,7 @@ public class TLCOutputInfo {
} }
public TLCOutputInfo(MachineContext machineContext, Renamer renamer, public TLCOutputInfo(MachineContext machineContext, Renamer renamer,
Typechecker typechecker, TLAModule tlaModule) { Typechecker typechecker, TLAModule tlaModule, ConfigFile configFile) {
this.namesMapping = new Hashtable<String, String>(); this.namesMapping = new Hashtable<String, String>();
this.typesTable = new Hashtable<String, BType>(); this.typesTable = new Hashtable<String, BType>();
...@@ -60,6 +63,7 @@ public class TLCOutputInfo { ...@@ -60,6 +63,7 @@ public class TLCOutputInfo {
identifiers.putAll(machineContext.getConstants()); identifiers.putAll(machineContext.getConstants());
identifiers.putAll(machineContext.getVariables()); identifiers.putAll(machineContext.getVariables());
identifiers.putAll(machineContext.getEnumValues()); identifiers.putAll(machineContext.getEnumValues());
//TODO add sets of modelvalues
for (Entry<String, Node> entry : identifiers.entrySet()) { for (Entry<String, Node> entry : identifiers.entrySet()) {
......
...@@ -7,6 +7,7 @@ import de.tlc4b.btypes.FunctionType; ...@@ -7,6 +7,7 @@ import de.tlc4b.btypes.FunctionType;
import de.tlc4b.btypes.PairType; import de.tlc4b.btypes.PairType;
import de.tlc4b.btypes.SetType; import de.tlc4b.btypes.SetType;
import de.tlc4b.btypes.StructType; import de.tlc4b.btypes.StructType;
import de.tlc4b.exceptions.NotSupportedException;
import tla2sany.semantic.OpDeclNode; import tla2sany.semantic.OpDeclNode;
import tlc2.tool.TLCState; import tlc2.tool.TLCState;
import tlc2.tool.TLCStateInfo; import tlc2.tool.TLCStateInfo;
...@@ -185,7 +186,7 @@ public class TracePrinter { ...@@ -185,7 +186,7 @@ public class TracePrinter {
} }
} }
return null; throw new NotSupportedException("Unkown type of tuple.");
case RECORDVALUE: { case RECORDVALUE: {
RecordValue rec = (RecordValue) val; RecordValue rec = (RecordValue) val;
...@@ -223,8 +224,11 @@ public class TracePrinter { ...@@ -223,8 +224,11 @@ public class TracePrinter {
case MODELVALUE: case MODELVALUE:
ModelValue modelValue = (ModelValue) val; ModelValue modelValue = (ModelValue) val;
String BName = tlcOutputInfo.getBName(modelValue.toString()); String bName = tlcOutputInfo.getBName(modelValue.toString());
res.append(BName); if(bName == null){
bName = modelValue.toString();
}
res.append(bName);
return res; return res;
case SETOFTUPLESVALUE: { case SETOFTUPLESVALUE: {
......
...@@ -33,7 +33,6 @@ public class SpecialTest { ...@@ -33,7 +33,6 @@ public class SpecialTest {
assertEquals(NoError, test(a)); assertEquals(NoError, test(a));
} }
@Test @Test
public void testConstantSetupFile2() throws Exception { public void testConstantSetupFile2() throws Exception {
String[] a = new String[] { String[] a = new String[] {
...@@ -49,7 +48,6 @@ public class SpecialTest { ...@@ -49,7 +48,6 @@ public class SpecialTest {
assertEquals(Deadlock, test(a)); assertEquals(Deadlock, test(a));
} }
@Test @Test
public void testDefinitionsLoad() throws Exception { public void testDefinitionsLoad() throws Exception {
String[] a = new String[] { String[] a = new String[] {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment