Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bad format of Json trace printing #47

Closed
tangruize opened this issue Sep 2, 2021 · 12 comments
Closed

Bad format of Json trace printing #47

tangruize opened this issue Sep 2, 2021 · 12 comments

Comments

@tangruize
Copy link

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
Copy link
Author

tangruize commented Sep 2, 2021

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
Copy link
Member

lemmy commented Sep 2, 2021

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

@lemmy
Copy link
Member

lemmy commented Sep 2, 2021

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

@lemmy lemmy reopened this Sep 2, 2021
lemmy added a commit that referenced this issue Sep 2, 2021
represented symbolically as an IntervalValue.

Fixes Github issue "Bad format of Json trace printing"
#47

[Bug]
lemmy added a commit that referenced this issue Sep 2, 2021
represented symbolically as an IntervalValue.

Fixes Github issue "Bad format of Json trace printing"
#47

[Bug]
@lemmy lemmy closed this as completed Sep 2, 2021
lemmy added a commit to tlaplus/tlaplus that referenced this issue Sep 2, 2021
represented symbolically as an IntervalValue.

Fixes Github issue "Bad format of Json trace printing"
tlaplus/CommunityModules#47

[Bug][TLC]
lemmy added a commit to tlaplus/Examples that referenced this issue Sep 2, 2021
lemmy added a commit to tlaplus/Examples that referenced this issue Sep 2, 2021
lemmy added a commit to tlaplus/Examples that referenced this issue Sep 2, 2021
@tangruize
Copy link
Author

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
Copy link
Member

lemmy commented Sep 3, 2021

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

lemmy added a commit that referenced this issue Sep 3, 2021
write to the same trace file concurrently.

#47

[Bug]
lemmy added a commit to tlaplus/tlaplus that referenced this issue Sep 3, 2021
@lemmy
Copy link
Member

lemmy commented Sep 3, 2021

Serializing to the Json file is a side-effect of evaluating the invariant. If multiple workers evaluate invariants concurrently, their writes interfere. Starting with 4619f8b and tlaplus/tlaplus@0c49038, writes are synchronized and the last write wins (overrides previous writes by other workers). With real-world specs, competing writes should be rare.

Workaround: Prepend the file name trace.json with e.g. TLC!Javatime. This approach would also work with TLC's -continue parameter.

@tangruize
Copy link
Author

Serializing to the Json file is a side-effect of evaluating the invariant.

Is it possible to serialize to the Json file without checking JsonInv? In some cases, such as deadlock, TLC exceptions, TLC prints the error trace but it cannot simply be captured by invariants.

@lemmy
Copy link
Member

lemmy commented Sep 3, 2021

This would be tlaplus/tlaplus#640 (comment). I'm happy to discuss details if you want to work on a PR. :-)

@lemmy
Copy link
Member

lemmy commented Sep 3, 2021

Btw. why do you care about Json formatting in the first place? Newer builds of TLC generate a trace spec for error traces on which users can easily evaluate trace expressions (see expression below):

---- MODULE DieHard_TTrace_1630686553 ----
EXTENDS Sequences, TLCExt, Toolbox, Naturals, TLC, DieHard

_expression ==
    LET DieHard_TEExpression == INSTANCE DieHard_TEExpression
    IN DieHard_TEExpression!expression
----

_trace ==
    LET DieHard_TETrace == INSTANCE DieHard_TETrace
    IN DieHard_TETrace!trace
----

_inv ==
    ~(
        TLCGet("level") = Len(_TETrace)
        /\
        small = (3)
        /\
        big = (4)
    )
----

_init ==
    /\ big = _TETrace[1].big
    /\ small = _TETrace[1].small
----

_next ==
    /\ \E i,j \in DOMAIN _TETrace:
        /\ \/ /\ j = i + 1
              /\ i = TLCGet("level")
        /\ big  = _TETrace[i].big
        /\ big' = _TETrace[j].big
        /\ small  = _TETrace[i].small
        /\ small' = _TETrace[j].small

\* Uncomment the ASSUME below to write the states of the error trace
\* to the given file in Json format. Note that you can pass any tuple
\* to `JsonSerialize`. For example, a sub-sequence of _TETrace.
    \* ASSUME
    \*     LET J == INSTANCE Json
    \*         IN J!JsonSerialize("DieHard_TTrace_1630686553.json", _TETrace)

=============================================================================

 Note that you can extract this module `DieHard_TEExpression`
  to a dedicated file to reuse `expression` (the module in the 
  dedicated `DieHard_TEExpression.tla` file takes precedence 
  over the module `BlockingQueue_TEExpression` below).

---- MODULE DieHard_TEExpression ----
EXTENDS Sequences, TLCExt, Toolbox, Naturals, TLC, DieHard

expression == 
    [
        \* To hide variables of the `DieHard` spec from the error trace,
        \* remove the variables below.  The trace will be written in the order
        \* of the fields of this record.
        big |-> big
        ,small |-> small
        
        \* Put additional constant-, state-, and action-level expressions here:
        \* ,_stateNumber |-> _TEPosition
        \* ,_bigUnchanged |-> big = big'
        
        \* Format the `big` variable as Json value.
        \* ,_bigJson |->
        \*     LET J == INSTANCE Json
        \*     IN J!ToJson(big)
        
        \* Lastly, you may build expressions over arbitrary sets of states by
        \* leveraging the _TETrace operator.  For example, this is how to
        \* count the number of times a spec variable changed up to the current
        \* state in the trace.
        \* ,_bigModCount |->
        \*     LET F[s \in DOMAIN _TETrace] ==
        \*         IF s = 1 THEN 0
        \*         ELSE IF _TETrace[s].big # _TETrace[s-1].big
        \*             THEN 1 + F[s-1] ELSE F[s-1]
        \*     IN F[_TEPosition - 1]
    ]

=============================================================================



Parsing and semantic processing can take forever if the trace below is long.
 In this case, it is advised to deserialize the trace from a binary file.
 To create the file, replace your spec's invariant F with:
  Inv == IF F THEN TRUE ELSE ~IOSerialize(Trace, "file.bin", TRUE)
 (IOUtils module is from https://modules.tlapl.us/)
\*
\*---- MODULE DieHard_TETrace ----
\*EXTENDS IOUtils, TLC, DieHard
\*
\*trace == IODeserialize("file.bin", TRUE)
\*
\*=============================================================================
\*

---- MODULE DieHard_TETrace ----
EXTENDS TLC, DieHard

trace == 
    <<
    ([small |-> 0,big |-> 0]),
    ([small |-> 0,big |-> 5]),
    ([small |-> 3,big |-> 2]),
    ([small |-> 0,big |-> 2]),
    ([small |-> 2,big |-> 0]),
    ([small |-> 2,big |-> 5]),
    ([small |-> 3,big |-> 4])
    >>
----


=============================================================================

---- CONFIG DieHard_TTrace_1630686553 ----

INVARIANT
    _inv

CHECK_DEADLOCK
    \* CHECK_DEADLOCK off because of PROPERTY or INVARIANT above.
    FALSE

INIT
    _init

NEXT
    _next

CONSTANT
    _TETrace <- _trace

ALIAS
    _expression
=============================================================================
\* Generated on Fri Sep 03 09:29:15 PDT 2021
markus@banana:~/examples/specifications/DieHard(master)$ alias tlc='java -Dtlc2.value.Values.width=1000 -Dutil.FileUtil.milliseconds=true -XX:+UseParallelGC -cp /opt/toolbox/tla2tools.jar tlc2.TLC'


markus@banana:~/examples/specifications/DieHard(master)$ tlc DieHard
TLC2 Version 2.16 of Day Month 20?? (rev: c824a8a)
Running breadth-first search Model-Checking with fp 59 and seed -6705806797176730866 with 1 worker on 16 cores with 7054MB heap and 64MB offheap memory [pid: 245017] (Linux 5.11.0-27-generic amd64, Ubuntu 11.0.11 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/markus/src/TLA/_specs/examples/specifications/DieHard/DieHard.tla
Parsing file /tmp/Naturals.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module DieHard
Starting... (2021-09-03 09:29:14)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2021-09-03 09:29:15.
Error: Invariant NotSolved is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ big = 0
/\ small = 0

State 2: <FillBigJug line 68, col 18 to line 69, col 34 of module DieHard>
/\ big = 5
/\ small = 0

State 3: <BigToSmall line 97, col 15 to line 98, col 48 of module DieHard>
/\ big = 2
/\ small = 3

State 4: <EmptySmallJug line 71, col 18 to line 72, col 30 of module DieHard>
/\ big = 2
/\ small = 0

State 5: <BigToSmall line 97, col 15 to line 98, col 48 of module DieHard>
/\ big = 0
/\ small = 2

State 6: <FillBigJug line 68, col 18 to line 69, col 34 of module DieHard>
/\ big = 5
/\ small = 2

State 7: <BigToSmall line 97, col 15 to line 98, col 48 of module DieHard>
/\ big = 4
/\ small = 3

73 states generated, 14 distinct states found, 1 states left on queue.
The depth of the complete state graph search is 7.
Finished in 01s at (2021-09-03 09:29:15)
Trace exploration spec path: ./DieHard_TTrace_1630686553.tla

markus@banana:~/examples/specifications/DieHard(master)$ tlc -config DieHard_TTrace_1630686553.tla DieHard_TTrace_1630686553.tla 
TLC2 Version 2.16 of Day Month 20?? (rev: c824a8a)
Running breadth-first search Model-Checking with fp 60 and seed 7508979940518507983 with 1 worker on 16 cores with 7054MB heap and 64MB offheap memory [pid: 245140] (Linux 5.11.0-27-generic amd64, Ubuntu 11.0.11 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/markus/src/TLA/_specs/examples/specifications/DieHard/DieHard_TTrace_1630686553.tla
Parsing file /tmp/Sequences.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/TLCExt.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Parsing file /tmp/Toolbox.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Toolbox.tla)
Parsing file /tmp/Naturals.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/TLC.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /home/markus/src/TLA/_specs/examples/specifications/DieHard/DieHard.tla
Parsing file /tmp/DieHard_TEExpression.tla (/home/markus/src/TLA/_specs/examples/specifications/DieHard/DieHard_TTrace_1630686553.tla)
Parsing file /tmp/DieHard_TETrace.tla (/home/markus/src/TLA/_specs/examples/specifications/DieHard/DieHard_TTrace_1630686553.tla)
Parsing file /tmp/FiniteSets.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module TLCExt
Semantic processing of module Toolbox
Semantic processing of module DieHard
Semantic processing of module DieHard_TEExpression
Semantic processing of module DieHard_TETrace
Semantic processing of module DieHard_TTrace_1630686553
Starting... (2021-09-03 09:29:38)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2021-09-03 09:29:39.
Error: Invariant _inv is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ big = 0
/\ small = 0

State 2: <_next line 30, col 5 to line 36, col 37 of module DieHard_TTrace_1630686553>
/\ big = 5
/\ small = 0

State 3: <_next line 30, col 5 to line 36, col 37 of module DieHard_TTrace_1630686553>
/\ big = 2
/\ small = 3

State 4: <_next line 30, col 5 to line 36, col 37 of module DieHard_TTrace_1630686553>
/\ big = 2
/\ small = 0

State 5: <_next line 30, col 5 to line 36, col 37 of module DieHard_TTrace_1630686553>
/\ big = 0
/\ small = 2

State 6: <_next line 30, col 5 to line 36, col 37 of module DieHard_TTrace_1630686553>
/\ big = 5
/\ small = 2

State 7: <_next line 30, col 5 to line 36, col 37 of module DieHard_TTrace_1630686553>
/\ big = 4
/\ small = 3

7 states generated, 7 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 7.
Finished in 01s at (2021-09-03 09:29:39)

@tangruize
Copy link
Author

Sorry for the late reply.

I am using TLC traces to generate test cases to test real code (motivated by eXtreme Modelling in Practice). Thus I need a portable format for scripts processing. Actually I didn't use Json format. I write a script to convert TLC traces to Python objects and it is enough to generate test cases.

If you are interested in this, I would be happy to introduce my work. Here is the GitHub repo. And some (potential) bugs of willemt/raft #118 are found by this method.

@lemmy
Copy link
Member

lemmy commented Oct 11, 2021

@tangruize This looks super interesting. Please go ahead and introduce your work.

@tangruize
Copy link
Author

Thank you for your attention! This topic may not be suitable to discuss in this issue. I'll send you an email at the end of this weekend.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

No branches or pull requests

2 participants