Bad format of Json trace printing

[tangruize]

Hello! I learned printing a TLC error trace in #json format and tried the EWD840_json example:

sed -i '/^SendMsg/{n;d;}' EWD840.tla  # delete '/\ active[i]' below SendMsg
wget -q https://nightly.tlapl.us/dist/tla2tools.jar \
           https://modules.tlapl.us/releases/latest/download/CommunityModules-deps.jar
java -jar tla2tools.jar EWD840_json

TLC prints Error: Evaluating invariant JsonInv failed. and the traces. The trace.json file content is:

[

Is there something I made a mistake?

It seems JsonInv should not be violated since TLCSet("exit", TRUE). I replaced JsonSerialize("trace.json", Trace) with TRUE and TLC shows that JsonInv is not violated.

I tried another example DieHard, which violates the Inv big /= 4. TLC prints no trace and there is a trace.json file. I think this should be the expected behavior?

But after repeatedly running DieHard, I found the trace.json can be bad formatted:

[
{"big":0,"small":0},
{"big":5,"small":0},
{"big":2,"small":3},
{"big":2,"small":0},
{"big":0,"small":2},
{"big":5,"small":2},
{"big":4,"small":3}
]
"big":1,"small":3},
{"big":4,"small":0}
]

After trying the above, I think Json.tla might has a bug if my operations are correct.

[tangruize]

Here is my environment setup:

$ uname -a
Linux linuxmint 5.4.0-80-generic #90-Ubuntu SMP Fri Jul 9 22:49:44 UTC 2021 x86_64 x86_64 x86_64 GNU/Linux

$ java -jar tla2tools.jar -version
TLC2 Version 2.16 of Day Month 20?? (rev: c070724)
Error: Error: unrecognized option: -version
Usage: java tlc2.TLC [-help] [-option] inputfile

I tried both Java 11 and Java 14.

$ java -version
openjdk version "11.0.11" 2021-04-20
OpenJDK Runtime Environment (build 11.0.11+9-Ubuntu-0ubuntu2.20.04)
OpenJDK 64-Bit Server VM (build 11.0.11+9-Ubuntu-0ubuntu2.20.04, mixed mode, sharing)

$ java -version
openjdk version "14.0.2" 2020-07-14
OpenJDK Runtime Environment (build 14.0.2+12-Ubuntu-120.04)
OpenJDK 64-Bit Server VM (build 14.0.2+12-Ubuntu-120.04, mixed mode, sharing)

TLC log:

TLC2 Version 2.16 of Day Month 20?? (rev: c070724)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 13 and seed 3505478062787136350 with 1 worker on 6 cores with 1444MB heap and 64MB offheap memory [pid: 10211] (Linux 5.4.0-80-generic amd64, Private Build 14.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Examples/specifications/ewd840/EWD840_json.tla
Parsing file /Examples/specifications/ewd840/EWD840.tla
Parsing file /tmp/TLC.tla (jar:file:/Examples/specifications/ewd840/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/TLCExt.tla (jar:file:/Examples/specifications/ewd840/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/Json.tla (jar:file:/Examples/specifications/ewd840/tla2tools.jar!/tla2sany/StandardModules/Json.tla)
Parsing file /tmp/Naturals.tla (jar:file:/Examples/specifications/ewd840/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /Examples/specifications/ewd840/SyncTerminationDetection.tla
Parsing file /tmp/Sequences.tla (jar:file:/Examples/specifications/ewd840/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/FiniteSets.tla (jar:file:/Examples/specifications/ewd840/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module SyncTerminationDetection
Semantic processing of module EWD840
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module TLCExt
Semantic processing of module Json
Semantic processing of module EWD840_json
Starting... (2021-09-02 11:57:21)
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Computed 128 initial states...
Computed 256 initial states...
Computed 512 initial states...
Finished computing initial states: 1024 distinct states generated at 2021-09-02 11:57:22.
Error: Evaluating invariant JsonInv failed.
Attempted to apply the operator overridden by the Java method
public static tlc2.value.impl.BoolValue tlc2.module.Json.serialize(tlc2.value.impl.StringValue,tlc2.value.impl.TupleValue) throws java.io.IOException,
but it produced the following error:
%2%
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white")
/\ tpos = 0
/\ tcolor = "black"

State 2: <InitiateProbe line 40, col 3 to line 45, col 43 of module EWD840>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white")
/\ tpos = 3
/\ tcolor = "white"

State 3: <PassToken line 58, col 3 to line 63, col 43 of module EWD840>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white")
/\ tpos = 2
/\ tcolor = "white"

State 4: <PassToken line 58, col 3 to line 63, col 43 of module EWD840>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> FALSE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white")
/\ tpos = 1
/\ tcolor = "white"

State 5: <SendMsg line 76, col 3 to line 79, col 31 of module EWD840>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "white")
/\ tpos = 1
/\ tcolor = "white"

Error: The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 15, column 5 to line 17, column 39 in EWD840_json
1. Line 16, column 8 to line 17, column 39 in EWD840_json
2. Line 16, column 17 to line 17, column 39 in EWD840_json
3. Line 16, column 20 to line 16, column 53 in EWD840_json
4. Line 16, column 48 to line 16, column 52 in EWD840_json


21370 states generated, 1408 distinct states found, 109 states left on queue.
The depth of the complete state graph search is 5.
Finished in 01s at (2021-09-02 11:57:22)
Trace exploration spec path: ./EWD840_json_TTrace_1630555041.tla

It seems that Json.tla is not overridden by CommunityModules-deps.jar.
And I noticed tlc2.value.impl.BoolValue tlc2.module.Json.serialize(tlc2.value.impl.StringValue,tlc2.value.impl.TupleValue) throws java.io.IOException in the TLC log.

[lemmy]

Thanks for reporting. This has nothing to do with the Json module but is a bug in TLCExt!Trace in recent tla2tools.jar.

[lemmy]

I take that back! This is indeed a bug in the Json module (that causes an otherwise unused code path leading to tlaplus/tlaplus#667. The Json module does not correctly handle the special case where the domain of a FcnRcdValue is represented "symbolically" by an IntervalValue instead of a Value[]. Related commits in TLC: tlaplus/tlaplus@d7c99ae tlaplus/tlaplus@c9f843c

[tangruize]

Thank you for fixing the bug so quickly! But the DieHard example still has problems:

[
{"big":0,"small":0},
{"big":5,"small":0},
{"big":2,"small":3},
{"big":2,"small":0},
{"big":0,"small":2},
{"big":5,"small":2},
{"big":4,"small":3}
]
"big":1,"small":3},
{"big":4,"small":0}
]

It appears with a probability of about 20%~40% in my computer. (It seems that traces of length 7 have no problem, but traces of length 9 have problems). Here are the CMDs to reproduce the problem:

git clone https://github.com/tangruize/tlc-cmd
cd tlc-cmd/examples/DieHard
for i in `seq 10`; do python3 ../../tlcwrapper.py DieHard_json.ini; done
# sudo apt install jq
find . -type f -name trace.json | xargs -I '{}' sh -c "jq empty '{}' || echo '{}'"

jq reports some files parse error.

Another problem, TLCSet("exit", FALSE) seems to have no effect. I replaced TLCSet("exit", FALSE) with FALSE to let TLC also report the error trace.

[lemmy]

Another problem, TLCSet("exit", FALSE) seems to have no effect. I replaced TLCSet("exit", FALSE) with FALSE to let TLC also report the error trace.

By design: https://github.com/tlaplus/tlaplus/blob/56fa5fabdd8b0ec99e51acfe58a74229ed3e2444/tlatools/org.lamport.tlatools/src/tlc2/module/TLCGetSet.java#L410-L419