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？<error.png>