From f4f1c83db980aeb067f74f69e8a8b7e842ae5691 Mon Sep 17 00:00:00 2001 From: Darius Foo Date: Thu, 17 Nov 2022 12:46:16 +0800 Subject: [PATCH] Remove Json module --- modules/Json.tla | 105 ----- modules/tlc2/overrides/Json.java | 464 ----------------------- modules/tlc2/overrides/TLCOverrides.java | 11 - tests/AllTests.tla | 1 - tests/JsonTests.tla | 163 -------- 5 files changed, 744 deletions(-) delete mode 100644 modules/Json.tla delete mode 100644 modules/tlc2/overrides/Json.java delete mode 100644 tests/JsonTests.tla diff --git a/modules/Json.tla b/modules/Json.tla deleted file mode 100644 index 340233e..0000000 --- a/modules/Json.tla +++ /dev/null @@ -1,105 +0,0 @@ --------------------------------- MODULE Json -------------------------------- - -LOCAL INSTANCE Sequences -LOCAL INSTANCE FiniteSets -LOCAL INSTANCE TLC - (*************************************************************************) - (* Imports the definitions from the modules, but doesn't export them. *) - (*************************************************************************) - ------------------------------------------------------------------------------ - -LOCAL IsSequence(F, D) == TRUE \/ FALSE - -LOCAL ToJsonKeyValue(F, d) == - ToString(ToString(d)) \o ":" \o ToString(F[d]) - -RECURSIVE ToJsonObjectString(_,_) -LOCAL ToJsonObjectString(F, D) == \* LOCAL just a hint for humans. - LET d == CHOOSE d \in D: TRUE - IN IF D = DOMAIN F - THEN "{" \o ToJsonKeyValue(F, d) \o IF D \ {d} = {} - THEN "}" - ELSE ToJsonObjectString(F, D \ {d}) - ELSE ", " \o ToJsonKeyValue(F, d) \o IF D \ {d} = {} - THEN "}" - ELSE ToJsonObjectString(F, D \ {d}) - -RECURSIVE ToJsonArrayString(_,_) -LOCAL ToJsonArrayString(F, D) == \* LOCAL just a hint for humans. - LET d == CHOOSE d \in D: TRUE - IN IF D = DOMAIN F - THEN "[" \o ToString(F[d]) \o IF D \ {d} = {} - THEN "]" - ELSE ToJsonArrayString(F, D \ {d}) - ELSE ", " \o ToString(F[d]) \o IF D \ {d} = {} - THEN "]" - ELSE ToJsonArrayString(F, D \ {d}) - -RECURSIVE ToJsonString(_,_) -LOCAL ToJsonString(F, D) == \* LOCAL just a hint for humans. - IF IsFiniteSet(F) \/ IsSequence(F, D) THEN - ToJsonArrayString(F, D) - ELSE - ToJsonObjectString(F, D) - -ToJson(value) == - (*************************************************************************) - (* Converts the given value to a JSON string. Records are converted to *) - (* JSON objects, tuples to JSON arrays, and scalar values as their JSON *) - (* representation. *) - (*************************************************************************) - IF DOMAIN value = {} THEN - "{}" - ELSE - ToJsonString(value, DOMAIN value) - -ToJsonArray(value) == - (*************************************************************************) - (* Converts the given tuple value to a JSON array. *) - (*************************************************************************) - IF DOMAIN value = {} THEN - "[]" - ELSE - ToJsonArrayString(value, DOMAIN value) - -ToJsonObject(value) == - (*************************************************************************) - (* Converts the given tuple value to a JSON object. *) - (*************************************************************************) - IF DOMAIN value = {} THEN - "{}" - ELSE - ToJsonObjectString(value, DOMAIN value) - -JsonSerialize(absoluteFilename, value) == - (*************************************************************************) - (* Serializes a tuple of values to the given file as (plain) JSON. *) - (* Records will be serialized as a JSON objects, and tuples as arrays. *) - (*************************************************************************) - TRUE - -JsonDeserialize(absoluteFilename) == - (*************************************************************************) - (* Deserializes JSON values from the given file. JSON objects will be *) - (* deserialized to records, and arrays will be deserialized to tuples. *) - (*************************************************************************) - CHOOSE val : TRUE - -ndJsonSerialize(absoluteFilename, value) == - (*************************************************************************) - (* Serializes a tuple of values to the given file as newline delimited *) - (* JSON. Records will be serialized as a JSON objects, and tuples as *) - (* arrays. *) - (*************************************************************************) - TRUE - -ndJsonDeserialize(absoluteFilename) == - (*************************************************************************) - (* Deserializes JSON values from the given file. JSON values must be *) - (* separated by newlines. JSON objects will be deserialized to records, *) - (* and arrays will be deserialized to tuples. *) - (*************************************************************************) - CHOOSE val : TRUE - -============================================================================= diff --git a/modules/tlc2/overrides/Json.java b/modules/tlc2/overrides/Json.java deleted file mode 100644 index eacc120..0000000 --- a/modules/tlc2/overrides/Json.java +++ /dev/null @@ -1,464 +0,0 @@ -package tlc2.overrides; -/******************************************************************************* - * Copyright (c) 2019 Microsoft Research. All rights reserved. - * - * The MIT License (MIT) - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies - * of the Software, and to permit persons to whom the Software is furnished to do - * so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS - * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR - * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN - * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION - * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. - * - * Contributors: - * Markus Alexander Kuppe - initial API and implementation - ******************************************************************************/ - -import java.io.BufferedReader; -import java.io.BufferedWriter; -import java.io.File; -import java.io.FileReader; -import java.io.FileWriter; -import java.io.IOException; -import java.util.ArrayList; -import java.util.Iterator; -import java.util.List; -import java.util.Map; - -import com.google.gson.JsonArray; -import com.google.gson.JsonElement; -import com.google.gson.JsonObject; -import com.google.gson.JsonParser; -import com.google.gson.JsonPrimitive; - -import tlc2.value.IValue; -import tlc2.value.impl.BoolValue; -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; - -/** - * Module overrides for operators to read and write JSON. - */ -public class Json { - - /** - * Encodes the given value as a JSON string. - * - * @param value the value to encode - * @return the JSON string value - */ - @TLAPlusOperator(identifier = "ToJson", module = "Json", warn = false) - public static StringValue toJson(final IValue value) throws IOException { - return new StringValue(getNode(value).toString()); - } - - /** - * Encodes the given value as a JSON array string. - * - * @param value the value to encode - * @return the JSON array string value - */ - @TLAPlusOperator(identifier = "ToJsonArray", module = "Json", warn = false) - public static StringValue toJsonArray(final IValue value) throws IOException { - return new StringValue(getArrayNode(value).toString()); - } - - /** - * Encodes the given value as a JSON object string. - * - * @param value the value to encode - * @return the JSON object string value - */ - @TLAPlusOperator(identifier = "ToJsonObject", module = "Json", warn = false) - public static StringValue toJsonObject(final IValue value) throws IOException { - return new StringValue(getObjectNode(value).toString()); - } - - /** - * Deserializes a tuple of newline delimited JSON values from the given path. - * - * @param path the JSON file path - * @return a tuple of JSON values - */ - @TLAPlusOperator(identifier = "ndJsonDeserialize", module = "Json", warn = false) - public static IValue ndDeserialize(final StringValue path) throws IOException { - List values = new ArrayList<>(); - try (BufferedReader reader = new BufferedReader(new FileReader(new File(path.val.toString())))) { - String line = reader.readLine(); - while (line != null) { - JsonElement node = JsonParser.parseString(line); - values.add(getValue(node)); - line = reader.readLine(); - } - } - return new TupleValue(values.toArray(new Value[values.size()])); - } - - /** - * Deserializes a tuple of *plain* JSON values from the given path. - * - * @param path the JSON file path - * @return a tuple of JSON values - */ - @TLAPlusOperator(identifier = "JsonDeserialize", module = "Json", warn = false) - public static IValue deserialize(final StringValue path) throws IOException { - JsonElement node = JsonParser.parseReader(new FileReader(new File(path.val.toString()))); - return getValue(node); - } - - /** - * Serializes a tuple of values to newline delimited 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 = "ndJsonSerialize", module = "Json", warn = false) - public synchronized static BoolValue ndSerialize(final StringValue path, final Value v) throws IOException { - TupleValue value = (TupleValue) v.toTuple(); - 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())))) { - for (int i = 0; i < value.elems.length; i++) { - writer.write(getNode(value.elems[i]).toString() + "\n"); - } - } - return BoolValue.ValTrue; - } - - /** - * Serializes a tuple of values to newline delimited 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 { - TupleValue value = (TupleValue) v.toTuple(); - 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"); - } - return BoolValue.ValTrue; - } - - /** - * Recursively converts the given value to a {@code JsonElement}. - * - * @param value the value to convert - * @return the converted {@code JsonElement} - */ - private static JsonElement getNode(IValue value) throws IOException { - if (value instanceof RecordValue) { - return getObjectNode((RecordValue) value); - } else if (value instanceof TupleValue) { - return getArrayNode((TupleValue) value); - } else if (value instanceof StringValue) { - return new JsonPrimitive(((StringValue) value).val.toString()); - } else if (value instanceof ModelValue) { - return new JsonPrimitive(((ModelValue) value).val.toString()); - } else if (value instanceof IntValue) { - return new JsonPrimitive(((IntValue) value).val); - } else if (value instanceof BoolValue) { - return new JsonPrimitive(((BoolValue) value).val); - } else if (value instanceof FcnRcdValue) { - return getObjectNode((FcnRcdValue) value); - } else if (value instanceof FcnLambdaValue) { - 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 { - throw new IOException("Cannot convert value: unsupported value type " + value.getClass().getName()); - } - } - - /** - * Returns a boolean indicating whether the given value is a valid sequence. - * - * @param value the value to check - * @return indicates whether the value is a valid sequence - */ - private static boolean isValidSequence(FcnRcdValue value) { - final Value[] domain = value.getDomainAsValues(); - for (Value d : domain) { - if (!(d instanceof IntValue)) { - return false; - } - } - value.normalize(); - for (int i = 0; i < domain.length; i++) { - if (((IntValue) domain[i]).val != (i + 1)) { - return false; - } - } - return true; - } - - /** - * Recursively converts the given value to an {@code JsonObject}. - * - * @param value the value to convert - * @return the converted {@code JsonElement} - */ - private static JsonElement getObjectNode(IValue value) throws IOException { - if (value instanceof RecordValue) { - return getObjectNode((RecordValue) value); - } else if (value instanceof TupleValue) { - return getObjectNode((TupleValue) value); - } else if (value instanceof FcnRcdValue) { - return getObjectNode((FcnRcdValue) value); - } else if (value instanceof FcnLambdaValue) { - return getObjectNode((FcnRcdValue) ((FcnLambdaValue) value).toFcnRcd()); - } else { - throw new IOException("Cannot convert value: unsupported value type " + value.getClass().getName()); - } - } - - /** - * Converts the given record value to a {@code JsonObject}, recursively converting values. - * - * @param value the value to convert - * @return the converted {@code JsonElement} - */ - private static JsonElement getObjectNode(FcnRcdValue value) throws IOException { - if (isValidSequence(value)) { - return getArrayNode(value); - } - - final Value[] domain = value.getDomainAsValues(); - JsonObject jsonObject = new JsonObject(); - for (int i = 0; i < domain.length; i++) { - Value domainValue = domain[i]; - if (domainValue instanceof StringValue) { - jsonObject.add(((StringValue) domainValue).val.toString(), getNode(value.values[i])); - } else { - jsonObject.add(domainValue.toString(), getNode(value.values[i])); - } - } - return jsonObject; - } - - /** - * Converts the given record value to an {@code JsonObject}. - * - * @param value the value to convert - * @return the converted {@code JsonElement} - */ - private static JsonElement getObjectNode(RecordValue value) throws IOException { - JsonObject jsonObject = new JsonObject(); - for (int i = 0; i < value.names.length; i++) { - jsonObject.add(value.names[i].toString(), getNode(value.values[i])); - } - return jsonObject; - } - - /** - * Converts the given tuple value to an {@code JsonObject}. - * - * @param value the value to convert - * @return the converted {@code JsonElement} - */ - private static JsonElement getObjectNode(TupleValue value) throws IOException { - JsonObject jsonObject = new JsonObject(); - for (int i = 0; i < value.elems.length; i++) { - jsonObject.add(String.valueOf(i), getNode(value.elems[i])); - } - return jsonObject; - } - - /** - * Recursively converts the given value to an {@code JsonArray}. - * - * @param value the value to convert - * @return the converted {@code JsonElement} - */ - private static JsonElement getArrayNode(IValue value) throws IOException { - if (value instanceof TupleValue) { - return getArrayNode((TupleValue) value); - } else if (value instanceof FcnRcdValue) { - return getArrayNode((FcnRcdValue) value); - } else if (value instanceof FcnLambdaValue) { - 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 { - throw new IOException("Cannot convert value: unsupported value type " + value.getClass().getName()); - } - } - - /** - * Converts the given tuple value to an {@code JsonArray}. - * - * @param value the value to convert - * @return the converted {@code JsonElement} - */ - private static JsonElement getArrayNode(TupleValue value) throws IOException { - JsonArray jsonArray = new JsonArray(value.elems.length); - for (int i = 0; i < value.elems.length; i++) { - jsonArray.add(getNode(value.elems[i])); - } - return jsonArray; - } - - /** - * Converts the given record value to an {@code JsonArray}. - * - * @param value the value to convert - * @return the converted {@code JsonElement} - */ - private static JsonElement getArrayNode(FcnRcdValue value) throws IOException { - if (!isValidSequence(value)) { - return getObjectNode(value); - } - - value.normalize(); - JsonArray jsonArray = new JsonArray(value.values.length); - for (int i = 0; i < value.values.length; i++) { - jsonArray.add(getNode(value.values[i])); - } - return jsonArray; - } - - /** - * Converts the given tuple value to an {@code JsonArray}. - * - * @param value the value to convert - * @return the converted {@code JsonElement} - */ - private static JsonElement getArrayNode(SetEnumValue value) throws IOException { - value.normalize(); - Value[] values = value.elems.toArray(); - JsonArray jsonArray = new JsonArray(values.length); - for (int i = 0; i < values.length; i++) { - jsonArray.add(getNode(values[i])); - } - return jsonArray; - } - - /** - * Recursively converts the given {@code JsonElement} to a TLC value. - * - * @param node the {@code JsonElement} to convert - * @return the converted value - */ - private static Value getValue(JsonElement node) throws IOException { - if (node.isJsonArray()) { - return getTupleValue(node); - } - else if (node.isJsonObject()) { - return getRecordValue(node); - } - else if (node.isJsonPrimitive()) { - JsonPrimitive primitive = node.getAsJsonPrimitive(); - if (primitive.isNumber()) { - return IntValue.gen(primitive.getAsInt()); - } - else if (primitive.isBoolean()) { - return new BoolValue(primitive.getAsBoolean()); - } - else if (primitive.isString()) { - return new StringValue(primitive.getAsString()); - } - } - else if (node.isJsonNull()) { - return null; - } - throw new IOException("Cannot convert value: unsupported JSON value " + node.toString()); - } - - /** - * Converts the given {@code JsonElement} to a tuple. - * - * @param node the {@code JsonElement} to convert - * @return the tuple value - */ - private static TupleValue getTupleValue(JsonElement node) throws IOException { - List values = new ArrayList<>(); - JsonArray jsonArray = node.getAsJsonArray(); - for (int i = 0; i < jsonArray.size(); i++) { - values.add(getValue(jsonArray.get(i))); - } - return new TupleValue(values.toArray(new Value[values.size()])); - } - - /** - * Converts the given {@code JsonElement} to a record. - * - * @param node the {@code JsonElement} to convert - * @return the record value - */ - private static RecordValue getRecordValue(JsonElement node) throws IOException { - List keys = new ArrayList<>(); - List values = new ArrayList<>(); - Iterator> iterator = node.getAsJsonObject().entrySet().iterator(); - while (iterator.hasNext()) { - Map.Entry entry = iterator.next(); - keys.add(UniqueString.uniqueStringOf(entry.getKey())); - values.add(getValue(entry.getValue())); - } - return new RecordValue(keys.toArray(new UniqueString[keys.size()]), values.toArray(new Value[values.size()]), - false); - } - - /** - * @deprecated It will be removed when this Class is moved to `TLC`. - */ - @Deprecated - final static void resolves() { - // See TLCOverrides.java - } -} diff --git a/modules/tlc2/overrides/TLCOverrides.java b/modules/tlc2/overrides/TLCOverrides.java index 7967afb..b403f8e 100644 --- a/modules/tlc2/overrides/TLCOverrides.java +++ b/modules/tlc2/overrides/TLCOverrides.java @@ -40,17 +40,6 @@ public class TLCOverrides implements ITLCOverrides { @SuppressWarnings("rawtypes") @Override public Class[] get() { - try { - // Remove `Json.resolves();` call when this Class is moved to `TLC`. - Json.resolves(); - return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class, - FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, - DyadicRationals.class, Statistics.class }; - } catch (NoClassDefFoundError e) { - // Remove this catch when this Class is moved to `TLC`. - System.out.println("gson dependencies of Json overrides not found, Json module won't work unless " - + "the libraries in the lib/ folder of the CommunityModules have been added to the classpath of TLC."); - } return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class, Statistics.class }; diff --git a/tests/AllTests.tla b/tests/AllTests.tla index 5d5901a..dc7875a 100644 --- a/tests/AllTests.tla +++ b/tests/AllTests.tla @@ -6,7 +6,6 @@ (***************************************************) EXTENDS SequencesExtTests, SVGTests, - JsonTests, BitwiseTests, IOUtilsTests, FiniteSetsExtTests, diff --git a/tests/JsonTests.tla b/tests/JsonTests.tla deleted file mode 100644 index d4b4ed6..0000000 --- a/tests/JsonTests.tla +++ /dev/null @@ -1,163 +0,0 @@ ------------------------------ MODULE JsonTests ----------------------------- -EXTENDS Json, Integers, Sequences, TLC, TLCExt - -ASSUME LET T == INSTANCE TLC IN T!PrintT("JsonTests") - -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]")) -ASSUME(AssertEq(ToJsonArray({1}), "[1]")) -ASSUME(AssertEq(ToJsonArray({"foo"}), "[\"foo\"]")) -ASSUME(AssertEq(ToJsonObject([a |-> TRUE, b |-> FALSE]), "{\"a\":true,\"b\":false}")) -ASSUME(AssertEq(ToJsonObject([a |-> 1]), "{\"a\":1}")) -ASSUME(AssertEq(ToJsonObject([a |-> "b"]), "{\"a\":\"b\"}")) - -\* Structural values -ASSUME(AssertEq(ToJson({3, 2, 1}), "[1,2,3]")) -ASSUME(AssertEq(ToJson(<<3, 2, 1>>), "[3,2,1]")) -ASSUME(AssertEq(ToJson([x \in {3, 2, 1} |-> 2 * x + 1]), "[3,5,7]")) -ASSUME(AssertEq(ToJson(3 :> "c" @@ 2 :> "b" @@ 1 :> "a"), "[\"a\",\"b\",\"c\"]")) -ASSUME(AssertEq(ToJson([ {2, 1} -> {"a", "b"} ]), "[[\"a\",\"a\"],[\"a\",\"b\"],[\"b\",\"a\"],[\"b\",\"b\"]]")) -ASSUME(AssertEq(ToJson([ {1, 0} -> {"a", "b"} ]), "[{\"0\":\"a\",\"1\":\"a\"},{\"0\":\"a\",\"1\":\"b\"},{\"0\":\"b\",\"1\":\"a\"},{\"0\":\"b\",\"1\":\"b\"}]")) -ASSUME(AssertEq(ToJson([a: {2, 1}, b: {"a", "b"}]), "[{\"a\":1,\"b\":\"a\"},{\"a\":1,\"b\":\"b\"},{\"a\":2,\"b\":\"a\"},{\"a\":2,\"b\":\"b\"}]")) -ASSUME(AssertEq(ToJson({2, 1} \X {"b", "a"}), "[[1,\"a\"],[1,\"b\"],[2,\"a\"],[2,\"b\"]]")) -ASSUME(AssertEq(ToJson(SUBSET {2, 1}), "[[],[1],[2],[1,2]]")) -ASSUME(AssertEq(ToJson(1..3), "[1,2,3]")) -ASSUME(AssertEq(ToJsonArray({3, 2, 1}), "[1,2,3]")) -ASSUME(AssertEq(ToJsonArray(<<3, 2, 1>>), "[3,2,1]")) -ASSUME(AssertEq(ToJsonArray([x \in {3, 2, 1} |-> 2 * x + 1]), "[3,5,7]")) -ASSUME(AssertEq(ToJsonArray(3 :> "c" @@ 2 :> "b" @@ 1 :> "a"), "[\"a\",\"b\",\"c\"]")) -ASSUME(AssertEq(ToJsonArray([ {2, 1} -> {"a", "b"} ]), "[[\"a\",\"a\"],[\"a\",\"b\"],[\"b\",\"a\"],[\"b\",\"b\"]]")) -ASSUME(AssertEq(ToJsonArray([ {1, 0} -> {"a", "b"} ]), "[{\"0\":\"a\",\"1\":\"a\"},{\"0\":\"a\",\"1\":\"b\"},{\"0\":\"b\",\"1\":\"a\"},{\"0\":\"b\",\"1\":\"b\"}]")) -ASSUME(AssertEq(ToJsonArray([a: {2, 1}, b: {"a", "b"}]), "[{\"a\":1,\"b\":\"a\"},{\"a\":1,\"b\":\"b\"},{\"a\":2,\"b\":\"a\"},{\"a\":2,\"b\":\"b\"}]")) -ASSUME(AssertEq(ToJsonArray({2, 1} \X {"b", "a"}), "[[1,\"a\"],[1,\"b\"],[2,\"a\"],[2,\"b\"]]")) -ASSUME(AssertEq(ToJsonArray(SUBSET {2, 1}), "[[],[1],[2],[1,2]]")) -ASSUME(AssertEq(ToJsonArray(1..3), "[1,2,3]")) -ASSUME(AssertEq(ToJsonObject([a |-> FALSE, b |-> 1]), "{\"a\":false,\"b\":1}")) -ASSUME(AssertEq(ToJsonObject("a" :> 1 @@ "b" :> 2 @@ "c" :> 3), "{\"a\":1,\"b\":2,\"c\":3}")) -ASSUME(AssertEq(ToJsonObject(1 :> "b" @@ 0 :> "c"), "{\"0\":\"c\",\"1\":\"b\"}")) - -\* Tests FcnRcdValue where the domain could be represented symbolically. -ASSUME(AssertEq(ToJsonObject([n \in 1..2 |-> "a"]), "[\"a\",\"a\"]")) - -\* Nested values -ASSUME(AssertEq(ToJsonObject([a |-> {<<1, 2>>}, b |-> [c |-> 3]]), "{\"a\":[[1,2]],\"b\":{\"c\":3}}")) - -\* Serializing and deserializing objects -ndTestObjects == - LET output == <<[a |-> 1, b |-> "a"], [a |-> 2, b |-> "b"], [a |-> 3, b |-> "c"]>> - IN - /\ ndJsonSerialize("build/json/test.json", output) - /\ LET input == ndJsonDeserialize("build/json/test.json") - IN - /\ Len(input) = 3 - /\ input[1].a = 1 - /\ input[1].b = "a" - /\ input[2].a = 2 - /\ input[2].b = "b" - /\ input[3].a = 3 - /\ input[3].b = "c" -ASSUME(ndTestObjects) - -\* Serializing and deserializing arrays -ndTestArrays == - LET output == << <<1, 2, 3>>, <<4, 5, 6>>, <<7, 8, 9>> >> - IN - /\ ndJsonSerialize("build/json/test.json", output) - /\ LET input == ndJsonDeserialize("build/json/test.json") - IN - /\ Len(input) = 3 - /\ input[1][1] = 1 - /\ input[1][2] = 2 - /\ input[1][3] = 3 - /\ input[2][1] = 4 - /\ input[2][2] = 5 - /\ input[2][3] = 6 - /\ input[3][1] = 7 - /\ input[3][2] = 8 - /\ input[3][3] = 9 -ASSUME(ndTestArrays) - -\* Serializing and deserializing primitive values -ndTestPrimitives == - LET output == <<1, 2, 3, 4>> - IN - /\ ndJsonSerialize("build/json/test.json", output) - /\ LET input == ndJsonDeserialize("build/json/test.json") - IN - /\ Len(input) = 4 - /\ input[1] = 1 - /\ input[2] = 2 - /\ input[3] = 3 - /\ input[4] = 4 -ASSUME(ndTestPrimitives) - -\* Serializing and deserializing objects -TestObjects == - LET output == <<[a |-> 1, b |-> "a"], [a |-> 2, b |-> "b"], [a |-> 3, b |-> "c"]>> - IN - /\ JsonSerialize("build/json/test.json", output) - /\ LET input == JsonDeserialize("build/json/test.json") - IN - /\ Len(input) = 3 - /\ input[1].a = 1 - /\ input[1].b = "a" - /\ input[2].a = 2 - /\ input[2].b = "b" - /\ input[3].a = 3 - /\ input[3].b = "c" -ASSUME(TestObjects) - -\* Serializing and deserializing arrays -TestArrays == - LET output == << <<1, 2, 3>>, <<4, 5, 6>>, <<7, 8, 9>> >> - IN - /\ JsonSerialize("build/json/test.json", output) - /\ LET input == JsonDeserialize("build/json/test.json") - IN - /\ Len(input) = 3 - /\ input[1][1] = 1 - /\ input[1][2] = 2 - /\ input[1][3] = 3 - /\ input[2][1] = 4 - /\ input[2][2] = 5 - /\ input[2][3] = 6 - /\ input[3][1] = 7 - /\ input[3][2] = 8 - /\ input[3][3] = 9 -ASSUME(TestArrays) - -\* Serializing and deserializing primitive values -TestPrimitives == - LET output == <<1, 2, 3, 4>> - IN - /\ JsonSerialize("build/json/test.json", output) - /\ LET input == JsonDeserialize("build/json/test.json") - IN - /\ Len(input) = 4 - /\ input[1] = 1 - /\ input[2] = 2 - /\ input[3] = 3 - /\ input[4] = 4 -ASSUME(TestPrimitives) - -\* Round trip with complex object -\* There is no way to encode sets in json (like in XML or EDN), this is why we don't use it here -RoundTrip == - LET output == <<[a |-> 3], 2, <<<<1, 2>>, "look">>, <<<<<<[b |-> [c |-> <<4, 5, 6>>]]>>>>>>>> - IN - /\ JsonSerialize("build/json/test.json", output) - /\ output = JsonDeserialize("build/json/test.json") -ASSUME(RoundTrip) -=============================================================================