Add generic Serialize and Deserialize operators to IOUtils.

[lemmy]

IOExec!IOSerialize serializes the given TLA+ value with Java's built-in serialization. Alternatively, IOUtils!IOExec provides a low-level mechanism to write to files (see example at the bottom). More specifically, the Json and CSV modules have dedicated serialization mechanisms.

As a long-term replacement, TLA+ should subsume serialization under:

---- MODULE IOUtils ----

Serialize(value,dest,serializer,options) ==
    (* value: TLA+ value to be serialized. *)
    (* dest: Destination to serialize to such as a file or URL. *)
    (* serializer: Identifier of the serializer to be used such as "CSV", "NDJSON", "JSON", "TXT". *)
    (* options: Record of serializer-specific options. *)
    CHOOSE r \in [exitValue : Int, stdout : STRING, stderr : STRING] : TRUE

Deserialize(src,serializer,options) ==
    CHOOSE v

====

The advantage of this high-level interface is that serialization/deserialization is independent of a particular serializer and always looks the same while allowing serializers to add additional features such as formatting:

\* Plaintext
Serialize("An ordinary TLA+ string", "file.txt", "TXT", [charset|-> "UTF-8", append |-> TRUE])

\* Java string formatting
Serialize(<<"abc", 42, {"x", "y"} >>, "file.txt", "PRINTF", [pattern |-> "%1$s#%2$s#%3$s", charset|-> "UTF-8", append |-> TRUE])

\* CSV
Serialize(<<23, 42 77, "foo", {1,2,3}>>, "file.csv", "CSV", [headers |-> <<"A", "B", "Name", "Elems">>, delimiter |-> "#", append |-> TRUE])

Variant: Serializer moved into options:

---- MODULE IOUtils ----

Serialize(value,dest,options) ==
    (* value: TLA+ value to be serialized. *)
    (* dest: Destination to serialize to such as a file or URL. *)
    (* options: Record of serializer-specific options. *)
    CHOOSE r \in [exitValue : Int, stdout : STRING, stderr : STRING] : TRUE

Deserialize(src,options) ==
    CHOOSE v

====

\* Plaintext
Serialize("An ordinary TLA+ string", "file.txt", [serializer |-> "TXT", charset|-> "UTF-8", append |-> TRUE])

Serializers will be loaded by some service loader mechanism.

---

\* This is not even platform independent.
IOExec( <<"bash", "-c",  "echo \"Some String\" > " \o "SomeFile.txt">>)

[afonsonf]

Created here a test with service loader: https://github.com/afonsonf/CommunityModules
Is what I did correct, and do you have any suggestions?

Also, is there any code formatting tool to use in this project?

[lemmy]

@afonsonf Looking at your prototype, I wonder if we should combine this loader mechanism with the existing loader for module overrides? For example, we could enhance TLC's module loader to load module overrides depending on constant parameters passed to the operator:

...

Inv ==
   Serialize("An ordinary TLA+ string", "file.txt", "TXT", [charset|-> "UTF-8", append |-> TRUE])

When processing this spec at startup, SpecProcessor could wire up the RawSerializer when it sees the "TXT" constant parameter in the AST. For that, we could extend the @TLAPlusOperator to match the module override on the parameter value. What do you think?

[afonsonf]

When processing this spec at startup, SpecProcessor could wire up the RawSerializer when it sees the "TXT" constant parameter in the AST. For that, we could extend the @TLAPlusOperator to match the module override on the parameter value. What do you think?

Uhm, that seems more complex to develop

What about creating a new module called serializers, and in there have all the serializers. The abstract serializer could be something like:

serialize(value, dest, serializer, options) ==
	case serializer = "RAW" -> RAWSerializer(value, dest, options)
	[]   serializer = "TXT" -> TXTSerializer(value, dest, options)
	[]   OTHER              -> FALSE

And then each serializer could have their implementation written in TLA, and if required, also an override in Serializer.java. What do you think?

[lemmy]

The TLA+ definition of serialize with the CASE above does not allow others to add serializers without changing CommunityModules (technically, one could re-define the module in which serializer is defined, though). Do you think we don't need to let others add serializers without contributing them to CM?

The implementation of what I proposed above should be fairly straightforward. It should boil down to extending the annotation and annotation processing. I could implement a prototype ~next week.

[afonsonf]

I have here yet another poc: https://github.com/afonsonf/CommunityModules/tree/poc2
Where you would call the serializer with the class name (https://github.com/afonsonf/CommunityModules/blob/poc2/tests/IOUtilsTests.tla), maybe there could also be some default class names.

For the annotation extension I'm still not sure how would you relate in the specprocessor the parameter of the operator and the annotation field. Not sure about extending the annotation only because the serializer, however if it is designed in a way that more new operators can used it, it would be nice.

[lemmy]

Counterproposal at lemmy/tlaplus@2249366

How two module overrides for the same operator would look like:

diff --git a/modules/IOUtils.tla b/modules/IOUtils.tla
index ef7487b..4f47864 100644
--- a/modules/IOUtils.tla
+++ b/modules/IOUtils.tla
@@ -10,6 +10,15 @@ IOSerialize(val, absoluteFilename, compress) == TRUE

 IODeserialize(absoluteFilename, compressed) == CHOOSE val : TRUE

+Serialize(value, dest, options) ==
+    (* value: TLA+ value to be serialized. *)
+    (* dest: Destination to serialize to such as a file or URL. *)
+    (* options: Record of serializer-specific options. *)
+    CHOOSE r \in [exitValue : Int, stdout : STRING, stderr : STRING] : TRUE
+
+Deserialize(src, options) ==
+    CHOOSE val : TRUE
+
 ----------------------------------------------------------------------------

 IOExec(command) ==
diff --git a/modules/tlc2/overrides/IOUtils.java b/modules/tlc2/overrides/IOUtils.java
index 8bd44fd..0f4e336 100644
--- a/modules/tlc2/overrides/IOUtils.java
+++ b/modules/tlc2/overrides/IOUtils.java
@@ -35,8 +35,14 @@ import java.util.HashMap;
 import java.util.List;
 import java.util.Map;

+import tla2sany.semantic.ExprOrOpArgNode;
 import tlc2.output.EC;
+import tlc2.tool.EvalControl;
 import tlc2.tool.EvalException;
+import tlc2.tool.TLCState;
+import tlc2.tool.coverage.CostModel;
+import tlc2.tool.impl.Tool;
+import tlc2.util.Context;
 import tlc2.value.IValue;
 import tlc2.value.ValueInputStream;
 import tlc2.value.ValueOutputStream;
@@ -52,7 +58,7 @@ import util.UniqueString;
 public class IOUtils {

        @TLAPlusOperator(identifier = "IODeserialize", module = "IOUtils", warn = false)
-       public static final IValue deserialize(final StringValue absolutePath, final BoolValue compress)
+       public static final IValue ioDeserialize(final StringValue absolutePath, final BoolValue compress)
                        throws IOException {
                final ValueInputStream vis = new ValueInputStream(new File(absolutePath.val.toString()), compress.val);
                try {
@@ -63,7 +69,7 @@ public class IOUtils {
        }

        @TLAPlusOperator(identifier = "IOSerialize", module = "IOUtils", warn = false)
-       public static final IValue serialize(final IValue value, final StringValue absolutePath, final BoolValue compress)
+       public static final IValue ioSerialize(final IValue value, final StringValue absolutePath, final BoolValue compress)
                        throws IOException {
                final ValueOutputStream vos = new ValueOutputStream(new File(absolutePath.val.toString()), compress.val);
                try {
@@ -73,6 +79,38 @@ public class IOUtils {
                }
                return BoolValue.ValTrue;
        }
+
+       @Evaluation(definition = "Serialize", module = "IOUtils", warn = false, silent = true, priority = 50)
+       public synchronized static Value serialize50(final Tool tool, final ExprOrOpArgNode[] args, final Context c,
+                       final TLCState s0, final TLCState s1, final int control, final CostModel cm) {
+               final IValue opts = tool.eval(args[2]);
+               if (opts instanceof RecordValue) {
+                       final RecordValue rv = (RecordValue) opts;
+                       final StringValue name = (StringValue) rv.apply(new StringValue("ser"), EvalControl.Clear);
+                       if ("frob".equals(name.getVal().toString())) {
+                               return new RecordValue(EXEC_NAMES, new Value[] { IntValue.ValZero, new StringValue("frob"), new StringValue("")  }, false);
+                       }
+               }
+               return null;
+       }
+
+
+       @Evaluation(definition = "Serialize", module = "IOUtils", warn = false, silent = true)
+       public synchronized static Value serialize100(final Tool tool, final ExprOrOpArgNode[] args, final Context c,
+                       final TLCState s0, final TLCState s1, final int control, final CostModel cm) {
+               final IValue opts = tool.eval(args[2]);
+
+               if (opts instanceof RecordValue) {
+                       final RecordValue rv = (RecordValue) opts;
+                       final StringValue name = (StringValue) rv.apply(new StringValue("ser"), EvalControl.Clear);
+                       if ("bar".equals(name.getVal().toString())) {
+//                             final IValue value = tool.eval(args[0]);
+//                             final IValue dest = tool.eval(args[1]);
+                               return new RecordValue(EXEC_NAMES, new Value[] { IntValue.ValZero, new StringValue("bar"), new StringValue("")  }, false);
+                       }
+               }
+               return null;
+       }

        static {
                // Eagerly lookup the environment, which is not going to change while the Java
diff --git a/tests/IOUtilsTests.tla b/tests/IOUtilsTests.tla
index b7d64c0..97565ab 100644
--- a/tests/IOUtilsTests.tla
+++ b/tests/IOUtilsTests.tla
@@ -1,5 +1,21 @@
 ---------------------------- MODULE IOUtilsTests ----------------------------
 EXTENDS IOUtils, TLC, TLCExt, Integers
+
+---------------------------------------------------------------------------------------------------------------------------
+
+ASSUME PrintT("IOUtilsTests!D")
+
+ASSUME(LET ret == Serialize("Hello World", "/dev/null", [ser |-> "bar"])
+                                                                                                                                IN /\ PrintT(ret)
+                                                                    /\ ret.exitValue = 0
+                                                                    /\ ret.stderr = ""
+                                                                    /\ ret.stdout = "bar")
+ASSUME(LET ret == Serialize("Hello World", "/dev/null", [ser |-> "frob"])
+                                                                                                                                IN /\ PrintT(ret)
+                                                                    /\ ret.exitValue = 0
+                                                                    /\ ret.stderr = ""
+                                                                    /\ ret.stdout = "frob")
+

 ASSUME PrintT("IOUtilsTests!A")
=============================================================================

[afonsonf]

Your proposal seems to be a good option, should we proceed with that idea?

[kuujo]

Yeah I would prefer that the API be left generic and potentially pluggable with new serializers... especially for extracting information from TLC to help build higher-level tools (e.g. I'm using this for test case generation). This is also one area in particular where everyone has a preference and/or language-specific limitations that need to be worked around, so it's best to remain agnostic if possible.

@lemmy I really love your proposal!

[lemmy]

Proposed functionality added to TLC with tlaplus/tlaplus@2249366 and tlaplus/tlaplus@f480341.

[lemmy]

@afonsonf Can you create a PR for the TLA+ Serialize and Deserialize operators and a Java module override (@Evaluation) that provides text-based serialization?

[afonsonf]

Yes, I will work on it

[lemmy]

Thanks everybody!

[lemmy]

FWIW: tlaplus/tlaplus@1eb8156 puts #53 and this work together. :-)

[lemmy]

Append Json (or any other format) to a dump file:

----- MODULE Foo ------
EXTENDS IOUtils, Json, Naturals, Sequences

FormatOpts ==
   [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>]

FileName ==
   "foo.ndjson"

ASSUME 
    /\ Serialize(ToJson({"a", "b", "c"}) \o "\n", FileName, FormatOpts).exitValue = 0
    /\ Serialize(ToJson([ i \in 11..20 |-> i * i ]) \o "\n", FileName, FormatOpts).exitValue = 0

====================

/cc @kuujo