tlaplus: Ability to save TLC error trace in user-defined formats

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:

java -cp tla2tools.jar tlc2.TLC -jsonTrace <specname>

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.

About this issue

Original URL
State: closed
Created 3 years ago
Reactions: 1
Comments: 17 (14 by maintainers)

Commits related to this issue

Ability to save TLC error trace in JSON format Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Feature][TLC][Changelog] — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format Evaluate POSTCONDITION also when liveness checking reports a counter-example. When final liveness checking on the complete (behavior) graph finds a cou... — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format Add TLCExt!CounterExample Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Feature][TLC][Changelog] — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format Add TLCExt!ToTrace(CounterExample) Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Feature][TLC][Changelog] — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format. Handle case that succState is null. Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Feature][TLC] — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format. Support evaluating multiple post-conditions (not exposed in the config file). Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 ... — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format. Pass a generic map of command-line parameters to Tool and SpecProcessor. Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Fea... — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format. Instantiate SpecObj outside of SpecProcessor. Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Feature][TLC] — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format. Add ability to dynamically add post-conditions on the command-line. Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Feature]... — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format. Add "-dumpTrace" parameter to TLC (currently support for json). Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Feature][TLC... — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format. Show error message instead of exception when -dumpTrace command lacks file sub-parameter. Part of Github issue #640 https://github.com/tlaplus/tlaplus... — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format. Print success *after* serialization. Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Feature][TLC] — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format. Add TLA+ ("tla") format. Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Feature][TLC] — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in JSON format. Document new -dumpTrace and -postCondition parameters in current-tools.md and command-line help. Part of Github issue #640 https://github.com/tlaplus/... — committed to tlaplus/tlaplus by lemmy 2 years ago
Ability to save TLC error trace in TLC's binary format. Part of Github issue #640 https://github.com/tlaplus/tlaplus/issues/640 [Feature][TLC] — committed to tlaplus/tlaplus by lemmy 2 years ago
Fall back to newly introduced TLCStateInfo#action if TLCState#hasAction is false. TLCState#hasAction is true if TLC is running simulation, or when debugging (-debugger) a spec in BFS mode. Part of G... — committed to tlaplus/tlaplus by lemmy 7 months ago

Most upvoted comments

From a user perspective, I would prefer to have a dedicated command line flag that dumps the error trace to a specified JSON file. This seems the most straightforward approach. I would prefer to not have to write extra commands in TLA+ just to dump an error trace to a file. Using the POSTCONDITION feature/syntax just feels too esoteric.

will62794 on Feb 3, 2022

This is done:

markus@avocado [BlockingQueue]
-> % tlc -note BlockingQueueTrace.tla -dumpTrace json BQ-$(date +%s).json
TLC2 Version 2.18 of Day Month 20?? (rev: 386eaa1)
Running breadth-first search Model-Checking with fp 52 and seed -2854446944189387096 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 32500] (Mac OS X 12.2.1 aarch64, Homebrew 17.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Users/markus/src/TLA/_specs/models/tutorials/BlockingQueue/BlockingQueueTrace.tla
[...]
Semantic processing of module BlockingQueueTrace
Starting... (2022-02-16 17:37:49)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2022-02-16 17:37:50.
Error: Action property line 74, col 17 to line 74, col 29 of module BlockingQueue is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ buffer = <<>>
/\ i = 1
/\ waitSet = {}

[...]

State 16: <put line 156, col 8 to line 166, col 73 of module BlockingQueueTrace>
/\ buffer = <<"p1", "p1", "p2">>
/\ i = 16
/\ waitSet = {}

"CounterExample written: BQ-1645061869.json"
2529 states generated, 1169 distinct states found, 63 states left on queue.
The depth of the complete state graph search is 16.
Finished in 00s at (2022-02-16 17:37:50)

markus@avocado [BlockingQueue]
-> % cat BQ-1645061869.json
[
{"buffer":[],"i":1,"waitSet":[]},
{"buffer":[],"i":2,"waitSet":["c1"]},
{"buffer":["p1"],"i":3,"waitSet":[]},
{"buffer":["p1","p1"],"i":4,"waitSet":[]},
{"buffer":["p1"],"i":5,"waitSet":[]},
{"buffer":["p1","p1"],"i":6,"waitSet":[]},
{"buffer":["p1"],"i":7,"waitSet":[]},
{"buffer":["p1","p1"],"i":8,"waitSet":[]},
{"buffer":["p1","p1","p1"],"i":9,"waitSet":[]},
{"buffer":["p1","p1","p1"],"i":10,"waitSet":["p1"]},
{"buffer":["p1","p1"],"i":11,"waitSet":[]},
{"buffer":["p1","p1","p1"],"i":12,"waitSet":[]},
{"buffer":["p1","p1","p1"],"i":13,"waitSet":["p1"]},
{"buffer":["p1","p1","p1"],"i":14,"waitSet":["p1","p2"]},
{"buffer":["p1","p1"],"i":15,"waitSet":["p1"]},
{"buffer":["p1","p1","p2"],"i":16,"waitSet":[]}
]

@konnov @danwt Adding support for ITFTrace is a matter of writing a TLA+ definition that converts the CounterExample into your format and serializing your format with JsonSerialize. The code-level changes will be a one-liner in (TLC.java](https://github.com/tlaplus/tlaplus/blob/386eaa19f4d610781a79c95730638ba193cec614/tlatools/org.lamport.tlatools/src/tlc2/TLC.java#L589-L595).

lemmy on Feb 17, 2022

/cc @konnov @andrey-kuprianov @danwt related to https://apalache.informal.systems/docs/adr/015adr-trace.html

lemmy on Feb 1, 2022

I’m happy to review a PR that adds a command-line flag as described in https://github.com/tlaplus/tlaplus/issues/640#issuecomment-869070134 that is based on the infrastructure provided in https://github.com/tlaplus/tlaplus/commit/b9ab320da557646d174528b5c92b995611378e6e.

lemmy on Feb 3, 2022