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

Re: [tlaplus] TLA+ verification trace question。

This question is being discussed at https://github.com/tlaplus/tlaplus/issues/717#issuecomment-1044921779.


On Feb 17, 2022, at 10:21 PM, zhi niu <zhiniu28@xxxxxxxxx> wrote:

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/5B945383-0040-4D3C-93E1-066EA6FCA84E%40lemmster.de.