diff --git a/modules/parsers/ExternalFunctionParser/ExternalFunctionParser.java b/modules/parsers/ExternalFunctionParser/ExternalFunctionParser.java new file mode 100644 index 0000000..da6c3f8 --- /dev/null +++ b/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 domain = new ArrayList<>(); + List 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); + } +} diff --git a/modules/parsers/ExternalFunctionParser/ExternalFunctionParser.tla b/modules/parsers/ExternalFunctionParser/ExternalFunctionParser.tla new file mode 100644 index 0000000..610b292 --- /dev/null +++ b/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 + +======================================= diff --git a/modules/parsers/ExternalFunctionParser/README.md b/modules/parsers/ExternalFunctionParser/README.md new file mode 100644 index 0000000..5f10ba5 --- /dev/null +++ b/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") +``` diff --git a/modules/parsers/ExternalFunctionParser/examples/ex0.txt b/modules/parsers/ExternalFunctionParser/examples/ex0.txt new file mode 100644 index 0000000..8e7329a --- /dev/null +++ b/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 diff --git a/modules/parsers/ExternalFunctionParser/examples/ex1.txt b/modules/parsers/ExternalFunctionParser/examples/ex1.txt new file mode 100644 index 0000000..fab69f5 --- /dev/null +++ b/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 diff --git a/modules/parsers/ExternalRecordParser/ExternalRecordParser.java b/modules/parsers/ExternalRecordParser/ExternalRecordParser.java new file mode 100644 index 0000000..4377197 --- /dev/null +++ b/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 fields = new ArrayList<>(); + List 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); + } +} diff --git a/modules/parsers/ExternalRecordParser/ExternalRecordParser.tla b/modules/parsers/ExternalRecordParser/ExternalRecordParser.tla new file mode 100644 index 0000000..d623eb0 --- /dev/null +++ b/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 + +===================================== diff --git a/modules/parsers/ExternalRecordParser/README.md b/modules/parsers/ExternalRecordParser/README.md new file mode 100644 index 0000000..c36c4bb --- /dev/null +++ b/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") +``` diff --git a/modules/parsers/ExternalRecordParser/examples/ex0.txt b/modules/parsers/ExternalRecordParser/examples/ex0.txt new file mode 100644 index 0000000..032ae34 --- /dev/null +++ b/modules/parsers/ExternalRecordParser/examples/ex0.txt @@ -0,0 +1,2 @@ +a : 42 +b : true diff --git a/modules/parsers/ExternalSeqRecordParser/ExternalSeqRecordParser.java b/modules/parsers/ExternalSeqRecordParser/ExternalSeqRecordParser.java new file mode 100644 index 0000000..e6fc7aa --- /dev/null +++ b/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 rcdSeq = new ArrayList<>(); + try { + String line = br.readLine(); + while (line != null) { + // initialize arrays for field values [fields] and [values] + List fields = new ArrayList<>(); + List 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 fields, List 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]))); + } + } +} diff --git a/modules/parsers/ExternalSeqRecordParser/ExternalSeqRecordParser.tla b/modules/parsers/ExternalSeqRecordParser/ExternalSeqRecordParser.tla new file mode 100644 index 0000000..b9fa910 --- /dev/null +++ b/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 + +======================================== diff --git a/modules/parsers/ExternalSeqRecordParser/README.md b/modules/parsers/ExternalSeqRecordParser/README.md new file mode 100644 index 0000000..e9c1231 --- /dev/null +++ b/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") +``` diff --git a/modules/parsers/ExternalSeqRecordParser/examples/ex0.txt b/modules/parsers/ExternalSeqRecordParser/examples/ex0.txt new file mode 100644 index 0000000..03a789d --- /dev/null +++ b/modules/parsers/ExternalSeqRecordParser/examples/ex0.txt @@ -0,0 +1,3 @@ +a : 42, b : true +a : -1, b : false +a : 0, b : true