[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TLA+ verification trace question。

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

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:

---- 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



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

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.