Add external parsers

modules/parsers/ExternalFunctionParser/ExternalFunctionParser.java

@@ -0,0 +1,37 @@
+import tlc2.value.impl.*;
+
+import java.io.*;
+import java.util.*;
+
+public class ExternalFunctionParser {
+  // @TLAPlusOperator(identifier = "ExFunParser", module = "ExternalFunctionParser")
+  public static Value ExFunParser(final StringValue absolutePath) throws IOException {
+    // read the log file at [absolutePath]
+    BufferedReader br = new BufferedReader(new FileReader(absolutePath.val.toString()));
+    // initialize arrays for input values [domain] and output [values]
+    List<IntValue> domain = new ArrayList<>();
+    List<IntValue> values = new ArrayList<>();
+    try {
+      String line = br.readLine();
+      while (line != null) {
+        // split string on seperator into array of input and output values
+        String[] lnarr = line.split(", ");
+        // first parsed value is an input
+        IntValue x = IntValue.gen(Integer.parseInt(lnarr[0]));
+        // check if [domain] already contains this value
+        if (!domain.contains(x)) {
+          // if unique, add this value
+          domain.add(x);
+          // second parsed value is the corresponding output
+          values.add(IntValue.gen(Integer.parseInt(lnarr[1])));
+        }
+        // else, skip it
+        line = br.readLine();
+      }
+    } finally {
+      br.close();
+    }
+    // return the function which maps each input to its corresponding output
+    return new FcnRcdValue(domain.toArray(new Value[0]), values.toArray(new Value[0]), true);
+  }
+}

modules/parsers/ExternalFunctionParser/ExternalFunctionParser.tla

@@ -0,0 +1,8 @@
+---- MODULE ExternalFunctionParser ----
+
+EXTENDS Integers, Sequences, TLC
+
+\* parses the log to a TLA+ function
+ExFunParser(path) == CHOOSE s \in [ Int -> Int ] : TRUE
+
+=======================================

modules/parsers/ExternalFunctionParser/README.md

@@ -0,0 +1,15 @@
+# External Function Parser
+
+This small project provides a utility for parsing an `int -> int` function, computed externally and supplied as a log of comma-separated input-output values (see [examples](./examples)). This function can then be injected it into a TLA+ spec as a `CONSTANT`.
+
+[ExternalFunctionParser.java](ExternalFunctionParser.java) defines the Java class `ExternalFunctionParser` containing the `ExFunParser` function which parses a log of input-output pairs into a TLA+ function
+
+[ExternalFunctionParser.tla](ExternalFunctionParser.tla) is a dummy declaration for the `ExFunParser` function which is overriden by the Java function of the same name
+
+## Note on TLA+ Toolbox
+
+When parsing any provided examples *from the TLA+ toolbox*, one must modify the path accordingly. For example, to parse the function in `./examples/ex0.txt` from the toolbox, we evaluate
+
+```
+ExFunParser("../../examples/ex0.txt")
+```

modules/parsers/ExternalFunctionParser/examples/ex0.txt

@@ -0,0 +1,8 @@
+-1, 0
+0, 1
+1, 2
+2, 3
+4, 5
+5, 11
+6, 13
+7, 15

modules/parsers/ExternalFunctionParser/examples/ex1.txt

@@ -0,0 +1,11 @@
+0, 0
+1, 2
+2, 4
+3, 6
+4, 8
+5, 10
+6, 12
+7, 14
+8, 16
+9, 18
+10, 20

modules/parsers/ExternalRecordParser/ExternalRecordParser.java

@@ -0,0 +1,36 @@
+import tlc2.value.impl.*;
+import util.UniqueString;
+
+import java.io.*;
+import java.util.*;
+
+public class ExternalRecordParser {
+  // @TLAPlusOperator(identifier = "ExRcdParser", module = "ExternalRecordParser")
+  public static Value ExRcdParser(final StringValue absolutePath) throws IOException {
+    // read the log file at [absolutePath]
+    BufferedReader br = new BufferedReader(new FileReader(absolutePath.val.toString()));
+    // initialize arrays for input values [domain] and output [values]
+    List<UniqueString> fields = new ArrayList<>();
+    List<Value> values = new ArrayList<>();
+    try {
+      String line = br.readLine();
+      while (line != null) {
+        // split string on seperator into array of filed and value
+        String[] lnarr = line.split(" : ");
+        // first parsed value is a field
+        fields.add(UniqueString.uniqueStringOf(lnarr[0]));
+        // second parsed value is the corresponding value
+        if (lnarr[1].equals("false") || lnarr[1].equals("true")) {
+          values.add(new BoolValue(Boolean.parseBoolean(lnarr[1])));
+        } else {
+          values.add(IntValue.gen(Integer.parseInt(lnarr[1])));
+        }
+        line = br.readLine();
+      }
+    } finally {
+      br.close();
+    }
+    // return the record which maps each field to its corresponding value
+    return new RecordValue(fields.toArray(new UniqueString[0]), values.toArray(new Value[0]), true);
+  }
+}

modules/parsers/ExternalRecordParser/ExternalRecordParser.tla

@@ -0,0 +1,8 @@
+---- MODULE ExternalRecordParser ----
+
+EXTENDS Integers, TLC
+
+\* parses the log to a TLA+ record
+ExRcdParser(path) == CHOOSE r \in [ a : Int, b : BOOLEAN ] : TRUE
+
+=====================================

modules/parsers/ExternalRecordParser/README.md

@@ -0,0 +1,15 @@
+# External Record Parser
+
+This small project provides a utility for parsing a record `[ a : Int, b : BOOLEAN ]`, computed externally and supplied as a log of newline-separated field-value pairs (see [examples](./examples)). This function can then be injected it into a TLA+ spec as a `CONSTANT`.
+
+[ExternalRecordParser.java](ExternalRecordParser.java) defines the Java class `ExternalRecordParser` containing the `ExRcdParser` function which parses a log of field-value pairs into a TLA+ function
+
+[ExternalRecordParser.tla](ExternalRecordParser.tla) is a dummy declaration for the `ExRcdParser` function which is overriden by the Java function of the same name
+
+## Note on TLA+ Toolbox
+
+When parsing any provided examples *from the TLA+ toolbox*, one must modify the path accordingly. For example, to parse the function in `./examples/ex0.txt` from the toolbox, we evaluate
+
+```
+ExRcdParser("../../examples/ex0.txt")
+```

modules/parsers/ExternalRecordParser/examples/ex0.txt

@@ -0,0 +1,2 @@
+a : 42
+b : true

modules/parsers/ExternalSeqRecordParser/ExternalSeqRecordParser.java

@@ -0,0 +1,44 @@
+import tlc2.value.impl.*;
+import util.UniqueString;
+
+import java.io.*;
+import java.util.*;
+
+public class ExternalSeqRecordParser {
+  // @TLAPlusOperator(identifier = "ExSeqRcdParser", module = "ExternalSeqRecordParser")
+  public static Value ExSeqRcdParser(final StringValue absolutePath) throws IOException {
+    // read the log file at [absolutePath]
+    BufferedReader br = new BufferedReader(new FileReader(absolutePath.val.toString()));
+    // initialize array for all parsed records
+    List<RecordValue> rcdSeq = new ArrayList<>();
+    try {
+      String line = br.readLine();
+      while (line != null) {
+        // initialize arrays for field values [fields] and [values]
+        List<UniqueString> fields = new ArrayList<>();
+        List<Value> values = new ArrayList<>();
+        // split string on seperator into array of filed and value
+        String[] lnarr = line.split(", ");
+        // parse each entry of [lnarr] as a field-value pair
+        parsePair(lnarr[0].split(" : "), fields, values);
+        parsePair(lnarr[1].split(" : "), fields, values);
+        // add record to the sequence
+        rcdSeq.add(new RecordValue(fields.toArray(new UniqueString[0]), values.toArray(new Value[0]), true));
+        line = br.readLine();
+      }
+    } finally {
+      br.close();
+    }
+    // return the aggregated sequence of records
+    return new TupleValue(rcdSeq.toArray(new Value[0]));
+  }
+
+  private static void parsePair(String[] pair, List<UniqueString> fields, List<Value> values) {
+    fields.add(UniqueString.uniqueStringOf(pair[0]));
+    if (pair[1].equals("false") || pair[1].equals("true")) {
+      values.add(new BoolValue(Boolean.parseBoolean(pair[1])));
+    } else {
+      values.add(IntValue.gen(Integer.parseInt(pair[1])));
+    }
+  }
+}

modules/parsers/ExternalSeqRecordParser/ExternalSeqRecordParser.tla

@@ -0,0 +1,8 @@
+---- MODULE ExternalSeqRecordParser ----
+
+EXTENDS Integers, Sequences, TLC
+
+\* parses the log to a TLA+ sequence of TLA+ records
+ExSeqRcdParser(path) == CHOOSE r \in Seq([ a : Int, b : BOOLEAN ]) : TRUE
+
+========================================

modules/parsers/ExternalSeqRecordParser/README.md

@@ -0,0 +1,15 @@
+# External Record Sequence Parser
+
+This small project provides a utility for parsing a sequence of records `[ a : Int, b : BOOLEAN ]`, computed externally and supplied as a log of newline-separated, comma-separated field-value pairs (see [examples](./examples)). This function can then be injected it into a TLA+ spec as a `CONSTANT`.
+
+[ExternalSeqRecordParser.java](ExternalSeqRecordParser.java) defines the Java class `ExternalSeqRecordParser` containing the `ExSeqRcdParser` function which parses a log of newline-separated, comma-separated field-value pairs into a TLA+ function
+
+[ExternalSeqRecordParser.tla](ExternalSeqRecordParser.tla) is a dummy declaration for the `ExSeqRcdParser` function which is overriden by the Java function of the same name
+
+## Note on TLA+ Toolbox
+
+When parsing any provided examples *from the TLA+ toolbox*, one must modify the path accordingly. For example, to parse the function in `./examples/ex0.txt` from the toolbox, we evaluate
+
+```
+ExSeqRcdParser("../../examples/ex0.txt")
+```

modules/parsers/ExternalSeqRecordParser/examples/ex0.txt

@@ -0,0 +1,3 @@
+a : 42, b : true
+a : -1, b : false
+a : 0, b : true