lemmy
commented
3 years ago The -jsonTrace parameter should be combined with -generateSpecTE into -trace tla, -trace json, and -trace tla,json. As to the implementation, would it be possible to build it with the new-ish tlc2.output.IMessagePrinterRecorder functionality?
Here is an example how -generateSpecTE work as of now:
---- 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 2021markus@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)
pfeodrippe
will62794
konnov
danwt
In some cases it would be helpful to have the ability to save the error trace generated by TLC in an easily parseable format (e.g. JSON) for use by other tools, scripts, applications, etc. I have implemented a minimal prototype of this, using the previously developed functionality from the Json community module. The prototype usage is:
which saves a JSON error trace file to
trace.json. Of course, the exact CLI interface could be worked out more carefully, but that is just one, basic idea. See an example trace.json file for a broken run of Peterson's algorithm.