[tlaplus] TLA+ verification trace question。

[zhi niu <zhiniu28@xxxxxxxxx>]

Hello, I am using TLA+ to implement trace verification, and output the following error, what is the reason?

background：
Ideally, the trace log collection is as follows（<<[myId |-> 3, sid |-> 2], [myId |-> 3, sid |-> 1], [myId |-> 2, sid |-> 1]>>）, but there is a problem with the interface I implemented, please help to solve it, thank you very much.

1.my trace log as follows：
myId:3,sid:2
myId:3,sid:1
myId:2,sid:1

2.ExternalSeqRecordParser.tla
---- MODULE ExternalSeqRecordParser ----

EXTENDS Integers, Sequences, TLC

* parses the log to a TLA+ sequence of TLA+ records
ExSeqRcdParser(path) == CHOOSE r \in Seq([myId:Int,sid:Int]):TRUE

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

3.ExternalSeqRecordParser.java

package tlc2.overrides;
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]))); } } /* * <<[myId |-> 3, sid |-> 2], [myId |-> 3, sid |-> 1], [myId |-> 2, sid |-> 1]>> */

}

4.TLA+ running produces the following error，why？

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d06c79f0-cbf6-4b33-9510-e9187d4e5849n%40googlegroups.com.