Fix TLC module override of Json module to handle TupleValues.

tlaplus · Sep 4, 2019 · b759431 · b759431
1 parent 3a30da2
commit b759431
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 15 deletions.
diff --git a/modules/Json.java b/modules/Json.java
@@ -24,27 +24,46 @@
  *   Markus Alexander Kuppe - initial API and implementation
  ******************************************************************************/
 
+import tlc2.value.IValue;
 import tlc2.value.impl.FcnRcdValue;
+import tlc2.value.impl.IntValue;
 import tlc2.value.impl.StringValue;
+import tlc2.value.impl.TupleValue;
 
 public class Json {
 
 	// (p1 :> 0 @@ p2 :> 0 @@ p3 :> 0)
 	// ->
 	// "{\"p1\":0, \"p2\":0, \"p3\":0}"
-	public static final StringValue ToJsonObject(final FcnRcdValue r) {
+	public static final StringValue ToJsonObject(final IValue v) {
 		final StringBuffer buf = new StringBuffer();
 		buf.append("{");
 
-		for (int i = 0; i < r.domain.length; i++) {
-			buf.append("\"");
-			buf.append(r.domain[i]);
-			buf.append("\"");
-
-			buf.append(":");
-			buf.append(r.values[i]);
-			if (i < r.domain.length - 1) {
-				buf.append(",");
+		if (v instanceof FcnRcdValue) {
+			final FcnRcdValue r = (FcnRcdValue) v;
+			for (int i = 0; i < r.domain.length; i++) {
+				buf.append("\"");
+				buf.append(r.domain[i]);
+				buf.append("\"");
+
+				buf.append(":");
+				buf.append(r.values[i]);
+				if (i < r.domain.length - 1) {
+					buf.append(",");
+				}
+			}
+		} else if (v instanceof TupleValue) {
+			final TupleValue t = (TupleValue) v;
+			for (int i = 0; i < t.elems.length; i++) {
+				buf.append("\"");
+				buf.append(IntValue.gen(i + 1));
+				buf.append("\"");
+
+				buf.append(":");
+				buf.append(t.elems[i]);
+				if (i < t.elems.length - 1) {
+					buf.append(",");
+				}
 			}
 		}
 

diff --git a/tests/JsonTests.tla b/tests/JsonTests.tla
@@ -1,9 +1,9 @@
 ----------------------------- MODULE JsonTests -----------------------------
-EXTENDS Json, TLC
+EXTENDS Json, TLCExt
 
-ASSUME(ToJsonObject(<< >>) = "{}")
-ASSUME(ToJsonObject([ i \in {0,1,3} |-> "a" ]) = "{\"0\":\"a\", \"1\":\"a\", \"3\":\"a\"}")
-ASSUME(ToJsonObject([ i \in {0,1} |-> "a" ]) = "{\"0\":\"a\", \"1\":\"a\"}")
-ASSUME(ToJsonObject([ i \in {1} |-> "a" ]) = "{\"1\":\"a\"}")
+ASSUME(AssertEq(ToJsonObject(<< >>), "{}"))
+ASSUME(AssertEq(ToJsonObject([ i \in {0,1,3} |-> "a" ]), "{\"0\":\"a\",\"1\":\"a\",\"3\":\"a\"}"))
+ASSUME(AssertEq(ToJsonObject([ i \in {0,1} |-> "a" ]), "{\"0\":\"a\",\"1\":\"a\"}"))
+ASSUME(AssertEq(ToJsonObject([ i \in {1} |-> "a" ]), "{\"1\":\"a\"}"))
 
 =============================================================================