Support serializing records (RecordValue) in addition to sequences

(TupleValues) in JsonSerialize operator.

A RecordValue is serialized to a Json object, with the record value's
(finite) domain of strings being the Json keys.

[Feature][TLC]

Signed-off-by: Markus Alexander Kuppe <[email protected]>

Author: lemmy

modules/tlc2/overrides/Json.java

@@ -159,31 +159,27 @@ public synchronized static BoolValue ndSerialize(final StringValue path, final V
   }
 
   /**
-   * Serializes a tuple of values to newline delimited JSON.
+   * Serializes a TLA+ TupleValue or RecordValue to JSON.
    *
    * @param path  the file to which to write the values
    * @param value the values to write
    * @return a boolean value indicating whether the serialization was successful
    */
   @TLAPlusOperator(identifier = "JsonSerialize", module = "Json", warn = false)
   public synchronized static BoolValue serialize(final StringValue path, final Value v) throws IOException {
-	final TupleValue value = (TupleValue) v.toTuple();
+	Value value = v.toTuple();
+	if (value == null) {
+		value = v.toRcd();
+	}
 	if (value == null) {
 		throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
-				new String[] { "second", "JsonSerialize", "sequence", Values.ppr(v.toString()) });
+				new String[] { "second", "JsonSerialize", "sequence or record", Values.ppr(v.toString()) });
 	}
-    File file = new File(path.val.toString());
+
+	final File file = new File(path.val.toString());
     if (file.getParentFile() != null) {file.getParentFile().mkdirs();} // Cannot create parent dir for relative path.
     try (BufferedWriter writer = new BufferedWriter(new FileWriter(new File(path.val.toString())))) {
-    	writer.write("[\n");
-		for (int i = 0; i < value.elems.length; i++) {
-			writer.write(getNode(value.elems[i]).toString());
-			if (i < value.elems.length - 1) {
-				// No dangling "," after last element.
-				writer.write(",\n");
-			}
-		}
-    	writer.write("\n]\n");
+    	writer.write(getNode(v).toString());
     }
     return BoolValue.ValTrue;
   }

tests/JsonTests.tla

@@ -161,6 +161,13 @@ RoundTrip ==
        /\ output = JsonDeserialize("build/json/test.json")
 ASSUME(RoundTrip)
 
+RoundTrip2 ==
+    LET output == [a |-> 3, b |-> [c |-> <<4, 5, 6>>]]
+    IN
+       /\ JsonSerialize("target/json/test.json", output)
+       /\ output = JsonDeserialize("target/json/test.json")
+ASSUME(RoundTrip2)
+
 \* Deserialize existing ndjson with trailing white spaces and (empty) newlines.
 
 ASSUME LET input == <<[a |-> 3], <<<<1, 2>>, "look">>, << <<[b |-> [c |-> <<4, 5, 6>>]]>> >> >>
@@ -169,21 +176,19 @@ ASSUME LET input == <<[a |-> 3], <<<<1, 2>>, "look">>, << <<[b |-> [c |-> <<4, 5
 -----
 
 ASSUME AssertError(
-           "The second argument of JsonSerialize should be a sequence, but instead it is:\n[a |-> 1, b |-> TRUE]",
-           JsonSerialize("target/json/test.json", [a |-> 1, b |-> TRUE] ))
+           "The second argument of JsonSerialize should be a sequence or record, but instead it is:\n{1, 2, 3}",
+           JsonSerialize("target/json/test.json", {1,2,3} ))
 
 ASSUME AssertError(
            "The second argument of ndJsonSerialize should be a sequence, but instead it is:\n[a |-> 1, b |-> TRUE]",
            ndJsonSerialize("target/json/test.json", [a |-> 1, b |-> TRUE] ))
 
-
 ASSUME AssertError(
-           "The second argument of JsonSerialize should be a sequence, but instead it is:\n42",
+           "The second argument of JsonSerialize should be a sequence or record, but instead it is:\n42",
            JsonSerialize("target/json/test.json", 42 ))
 
 ASSUME AssertError(
            "The second argument of ndJsonSerialize should be a sequence, but instead it is:\n42",
            ndJsonSerialize("target/json/test.json", 42 ))
 
-
 =============================================================================