diff --git a/modules/tlc2/overrides/Json.java b/modules/tlc2/overrides/Json.java index cabf4ed..1760de1 100644 --- a/modules/tlc2/overrides/Json.java +++ b/modules/tlc2/overrides/Json.java @@ -42,7 +42,10 @@ import com.google.gson.JsonParser; import com.google.gson.JsonPrimitive; +import tlc2.output.EC; +import tlc2.tool.EvalException; import tlc2.value.IValue; +import tlc2.value.Values; import tlc2.value.impl.BoolValue; import tlc2.value.impl.FcnLambdaValue; import tlc2.value.impl.FcnRcdValue; @@ -144,7 +147,11 @@ public static IValue deserialize(final StringValue path) throws IOException { */ @TLAPlusOperator(identifier = "ndJsonSerialize", module = "Json", warn = false) public synchronized static BoolValue ndSerialize(final StringValue path, final Value v) throws IOException { - TupleValue value = (TupleValue) v.toTuple(); + final TupleValue value = (TupleValue) v.toTuple(); + if (value == null) { + throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, + new String[] { "second", "ndJsonSerialize", "sequence", Values.ppr(v.toString()) }); + } 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())))) { @@ -164,7 +171,11 @@ 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 { - TupleValue value = (TupleValue) v.toTuple(); + final TupleValue value = (TupleValue) v.toTuple(); + if (value == null) { + throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, + new String[] { "second", "JsonSerialize", "sequence", Values.ppr(v.toString()) }); + } 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())))) { diff --git a/tests/JsonTests.tla b/tests/JsonTests.tla index 74c84bc..46d800c 100644 --- a/tests/JsonTests.tla +++ b/tests/JsonTests.tla @@ -166,4 +166,24 @@ ASSUME(RoundTrip) ASSUME LET input == <<[a |-> 3], <<<<1, 2>>, "look">>, << <<[b |-> [c |-> <<4, 5, 6>>]]>> >> >> IN input = ndJsonDeserialize("tests/JsonTests.ndjson") +----- + +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] )) + +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", + 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 )) + + =============================================================================