Serialize model values as strings

Author: jobvs

modules/tlc2/overrides/Json.java

@@ -51,6 +51,7 @@
 import tlc2.value.impl.FcnRcdValue;
 import tlc2.value.impl.IntValue;
 import tlc2.value.impl.IntervalValue;
+import tlc2.value.impl.ModelValue;
 import tlc2.value.impl.RecordValue;
 import tlc2.value.impl.SetEnumValue;
 import tlc2.value.impl.SetOfFcnsValue;
@@ -153,6 +154,8 @@ private static JsonNode getNode(IValue value) throws IOException {
       return getArrayNode((TupleValue) value);
     } else if (value instanceof StringValue) {
       return new TextNode(((StringValue) value).val.toString());
+    } else if (value instanceof ModelValue) {
+      return new TextNode(((ModelValue) value).val.toString());
     } else if (value instanceof IntValue) {
       return new IntNode(((IntValue) value).val);
     } else if (value instanceof BoolValue) {

tests/AllTests.cfg

@@ -0,0 +1 @@
+CONSTANT ModelValueConstant = ModelValue

tests/JsonTests.tla

@@ -1,13 +1,17 @@
 ----------------------------- MODULE JsonTests -----------------------------
 EXTENDS Json, Integers, Sequences, TLC, TLCExt
 
+CONSTANT ModelValueConstant
+
 \* Empty values
 ASSUME(AssertEq(ToJsonArray({}), "[]"))
 ASSUME(AssertEq(ToJsonArray(<<>>), "[]"))
 
 \* Primitive values
 ASSUME(AssertEq(ToJson(FALSE), "false"))
 ASSUME(AssertEq(ToJson(1), "1"))
+ASSUME(AssertEq(ToJson("a"), "\"a\""))
+ASSUME(AssertEq(ToJson(ModelValueConstant), "\"ModelValue\""))
 ASSUME(AssertEq(ToJson({TRUE, FALSE}), "[false,true]"))
 ASSUME(AssertEq(ToJson({1}), "[1]"))
 ASSUME(AssertEq(ToJsonArray({TRUE, FALSE}), "[false,true]"))