diff --git a/modules/tlc2/overrides/Json.java b/modules/tlc2/overrides/Json.java index 4620403..bd831a0 100644 --- a/modules/tlc2/overrides/Json.java +++ b/modules/tlc2/overrides/Json.java @@ -159,7 +159,7 @@ 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 @@ -167,23 +167,19 @@ public synchronized static BoolValue ndSerialize(final StringValue path, final V */ @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; } diff --git a/tests/JsonTests.tla b/tests/JsonTests.tla index 46d800c..8af2f1d 100644 --- a/tests/JsonTests.tla +++ b/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 )) - =============================================================================