From 78ab86c8c2ae1b9c175c8f20dfc1789a639d239c Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Tue, 27 May 2014 20:27:50 +0200
Subject: [PATCH] Fixed a bug in the TracePrinter
---
src/main/java/de/tlc4b/Translator.java | 2 +-
src/main/java/de/tlc4b/tlc/TLCOutputInfo.java | 8 ++++++--
src/main/java/de/tlc4b/tlc/TracePrinter.java | 10 +++++++---
.../java/de/tlc4b/tlc/integration/SpecialTest.java | 2 --
4 files changed, 14 insertions(+), 8 deletions(-)
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 5ee1456..911a863 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 69e2371..6be0cea 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 9260f4d..4bf91aa 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 180a913..a078bd7 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[] {
--
GitLab