From 0f9cf8a1b7fa08a7ed9d821a7c6f8d8f605936dc Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Fri, 15 Dec 2023 15:45:36 -0800
Subject: [PATCH] Json module doesn't support serializing instances of type
 SetPredValue.

Ports fix of tlaplus/tlaplus Github issue #849
https://github.com/tlaplus/tlaplus/issues/849

[Bug]
---
 modules/tlc2/overrides/Json.java | 30 +++++-------------------------
 1 file changed, 5 insertions(+), 25 deletions(-)

diff --git a/modules/tlc2/overrides/Json.java b/modules/tlc2/overrides/Json.java
index 1760de1..4620403 100644
--- a/modules/tlc2/overrides/Json.java
+++ b/modules/tlc2/overrides/Json.java
@@ -47,18 +47,14 @@
 import tlc2.value.IValue;
 import tlc2.value.Values;
 import tlc2.value.impl.BoolValue;
+import tlc2.value.impl.EnumerableValue;
 import tlc2.value.impl.FcnLambdaValue;
 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;
-import tlc2.value.impl.SetOfRcdsValue;
-import tlc2.value.impl.SetOfTuplesValue;
 import tlc2.value.impl.StringValue;
-import tlc2.value.impl.SubsetValue;
 import tlc2.value.impl.TupleValue;
 import tlc2.value.impl.Value;
 import util.UniqueString;
@@ -217,16 +213,8 @@ private static JsonElement getNode(IValue value) throws IOException {
       return getObjectNode((FcnRcdValue) ((FcnLambdaValue) value).toFcnRcd());
     } else if (value instanceof SetEnumValue) {
       return getArrayNode((SetEnumValue) value);
-    } else if (value instanceof SetOfRcdsValue) {
-      return getArrayNode((SetEnumValue) ((SetOfRcdsValue) value).toSetEnum());
-    } else if (value instanceof SetOfTuplesValue) {
-      return getArrayNode((SetEnumValue) ((SetOfTuplesValue) value).toSetEnum());
-    } else if (value instanceof SetOfFcnsValue) {
-      return getArrayNode((SetEnumValue) ((SetOfFcnsValue) value).toSetEnum());
-    } else if (value instanceof SubsetValue) {
-      return getArrayNode((SetEnumValue) ((SubsetValue) value).toSetEnum());
-    } else if (value instanceof IntervalValue) {
-      return getArrayNode((SetEnumValue) ((IntervalValue) value).toSetEnum());
+    } else if (value instanceof EnumerableValue) {
+      return getArrayNode((SetEnumValue) ((EnumerableValue) value).toSetEnum());
     } else {
       throw new IOException("Cannot convert value: unsupported value type " + value.getClass().getName());
     }
@@ -341,16 +329,8 @@ private static JsonElement getArrayNode(IValue value) throws IOException {
       return getArrayNode((FcnRcdValue) ((FcnLambdaValue) value).toFcnRcd());
     } else if (value instanceof SetEnumValue) {
       return getArrayNode((SetEnumValue) value);
-    } else if (value instanceof SetOfRcdsValue) {
-      return getArrayNode((SetEnumValue) ((SetOfRcdsValue) value).toSetEnum());
-    } else if (value instanceof SetOfTuplesValue) {
-      return getArrayNode((SetEnumValue) ((SetOfTuplesValue) value).toSetEnum());
-    } else if (value instanceof SetOfFcnsValue) {
-      return getArrayNode((SetEnumValue) ((SetOfFcnsValue) value).toSetEnum());
-    } else if (value instanceof SubsetValue) {
-      return getArrayNode((SetEnumValue) ((SubsetValue) value).toSetEnum());
-    } else if (value instanceof IntervalValue) {
-      return getArrayNode((SetEnumValue) ((IntervalValue) value).toSetEnum());
+    } else if (value instanceof EnumerableValue) {
+      return getArrayNode((SetEnumValue) ((EnumerableValue) value).toSetEnum());
     } else {
       throw new IOException("Cannot convert value: unsupported value type " + value.getClass().getName());
     }