[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] TLA+ verification trace question。
- From: zhi niu <zhiniu28@xxxxxxxxx>
- Date: Thu, 17 Feb 2022 22:21:27 -0800 (PST)
- Ironport-data: A9a23:bUdAt6ig401KLK3bEPs4LNbnX1618RUKZh0ujC45NGQN5FlHY01je htvXGzTa//eazT3e4twbo6x/UgH6JOGmt9jHQo/rCphRSpjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UKidUsxIbVcMpB0J0HqPoMZkxN446TSFK1nV4 4mq+ZSAYATNNwNcawr41YrT8HuDg9yp4Fv0jnRmDRyclAK2e9E9VfrzFInpR5fKatE88t2SG 44v+IqEElbxpH/BPD8KfoHTKSXmSpaKVeSHZ+E/t6KK2nCurQRquko32WZ1hUp/0120c95NJ Nplr8OARAx4GKzwifkdDRNyHj0gAPxd5+qSSZS/mZT7I0zudnLtx7BpDRhzM9RJo6B4BmZB8 fFeIzcIBvyBr7jukfTrF6812JtldZiyVG8ckikIITXxEfIvWZTeWObA49Ry92gSoPpjNq33T fAzMxpRXC/hSjhgA3oyKq0PpN6Brnb4dDJcpV2Porcv+C7YywkZPL3FboCFIYTWFa25mG6di lnt3X3iCysZbsezkiq9wnWS2vDQyHaTtIU6TeXkrJaGmma7ym0IAwANTnOnpfD/j1WkHtNZM U0dvCsot6k7skKxJuQRRDW9qX+A+xkdAp9eSrxjrg6KzaXQ7kCSAW1soiN9hMIOrpAGSDd78 F61js7pWzZFvaHLdCOG6eLBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zQMZZafWlSVnNL yC2QDsW3OpM0JZav0mv1RWW3GL2/8mhohsdv12PBgqYAhVFiJlJjrFEBHDe5PdEaYGYFxyP5 Sld3ceZ6+8KANeGkynlrAQx8FOBuKzt3N702wUH83wdG9KFpyHLkWd4vWkWGauRGpxYEQIFm WeK0e+r2LddPWGxcYh8aJ+rBsIhwMDITIq5C6mONIQWOsQgKGdrGR2Cg2bAjwgBd2B8wckC1 WuzLK5A8F5GU/08lGPuLwvj+eZzmXxvrY8seXwL503/jeD2iI+9RrACP1+DBt3VH4vVyDg5B +13bpPUoz0GCbGWSnSJreY7cA5bRVBmVcGeg5EGKoarf1s2cEl/UKW56e16JORYc1F9x48kC FngAhcAoLc+7FWcQTi3hodLMu23Bs8n9SphVcHuVH7xs0UejU+UxP93X/MKkXMProSPFNZ4E KsIfduuGPNKRmiV8jgRd8Cj/oNlcxuviA2UODe9e340eJs5H17F/drtfw3O8igSD3vn7pBn+ OL+iQ6LE4AeQwlCDdrNbK79xV2Gu3VAyvl5WFHFI4UOdUi1qNpqJiX9g+UZOcYJLRmflDKW2 xzHUxgdrOjJ5YQy9YCR16yDqo6oFcp4H1ZbTzGLt+boaXGC8zP6k4FaUeuOcTTMb0/O+f2vN bdP0vXxEPwbh1IV4YdxFrBcy6hhtdbiorltyBs9QCfGYlGtPbNXInec2P5JuKAQlKRSvhG7W x7W99RXYO7bOM7sHFMLHgc9avWf0vUYxmvb4fgveRuo6yhw876KXl9VIgGXzidaKeItYo8ix O4gvu8Q6hC+20pxaY/d0X4L+jTeNGEEXoUmqooeXN3hhD0txwwQepfbECL3vMyCZtgQYEknJ jiY2PjLi7hGnBaQdnMyET3K3LMYi81f4VZFy1gNI1nPkd3A36dl0BpU+DUxbwJU0hQXjL4pa zYzbxV4dfeU4jNlpMlfRGTwSQtPMxuUpx7qwFwTmWyFEkSlBz7JLXYhBOCW4Uod/z4OdzRX5 u/ImmPsUDL2e5P+2Sw9XUNqsfv+Vcc08wTEkc+qXJ/aT8hmPGS13fb3OykVrQD6C9g6nkzNq MFl++F/baD0LykNu7Z9AI6fjOxCRBeBLW1EYPdg4KJYTTqHIWrth2eDexKrZ8dAB/3W6kvkW cZgEcRCCkal3yGUozFHWKMBL+MmlfIl/oZTKLP3OXYd4fzYoSBurYrLsCf5g2AvTpNllsN6J ZnWairFDmiZnX9JgCjWscNfMXC5a9QJaVGuxuyz6+lVRZsPvPs2LRM327qw+nKUaU5ppkPN+ gzEYKDSwqppzoE1x9ngFaBKBgOVL9LvVbTXrFri7YwWNd6fY93Tsw41q0X8O1gEN7UmXdkqx 6+Gt8T63R+Ysbs7O4wDd0Jty0WUCQSOsOtr3gbfKXBbmW6FWZap7UJSoia3LptGlN4b7c6iL +d9hA1cavZNM+qxBlUMA8SdL/rZI6vwaajkqCynqOmUEV4W1gmvwBaP6yrydW8CHsMXE8SWN +I30spCIvhXq4NDABILHfZ7G4Q+K1jmMUfjmxsdqhHAZlSVbpi+VncOWPbuBfwnypVJLSoi3 a/4ew==
- Ironport-hdrordr: A9a23:7UwQxaFmyyFIQWY8pLqEd8eALOsnbusQ8zAXPiFKOGZom6mj/a 2TdZsgpHvJYVoqKRYdcT7pAtj1fZvznaQFlLX5fo3SLTUPgQOTXfNfBPLZskrd8k7Fh5VgPR IKSdkBNDSPNykCsS+g2njGLz9I+rDum9HLuQ659QYQcehEUc5dBmxCe36m+yNNNW977VtQLu v+2iOFnVSdkLYsAvhSthI+Lpv+ThHw9a4PkXU9dmMaAcC17ULM1JfKVyKA1hNbeTJCy7Uv/C zklEjW/aO+qpiAu2/h61M=
- Ironport-sdr: r5Ssb6fyxmzeNMmvYmHA/yMDFrmv58Eq9DbzLXpzPF7zRYb05TiW/k3mrmE/I15DiPGe+OVewM RqcPduQt29T3S6pihyTDMY6rccsmo0U3j/O0AQPkYusU+8UsU97bs0akg6TJKAB6liT+ytJ8MS 6x6av4qZBqwOoj8LQrDnjfoHUmiDLA3R+VMAWNgfS9mNL0SVOHziNIWJ3Z0qz2y9fOGt/0Zuv+ vGDY2Y2roin3762pLVLPpinp8xNkNS8fk2VM+a2utL8OipS5z8nabrONH61ZJKb4VlyzHTnSek TtyJgXqP9RYBioFmmvrIPH4y
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.